Re: [isabelle] mutually recursion problem



On 01.07.2011 03:39, Данијела Петровић wrote:
As you can see there are actually two lemmas, but they are "mutually
recursive" (because the functions point_poly and line_poly that I previously
defined are mutually recursive). The problem is that when i try to prove
like this, then this 'arbitrary:state' only affects the first lemma, but not
the second one, and that is not convenient at all. Any suggestions how to
solve this?

You probably need to give arbitrary a list for each of the goals, separated by "and": So try using "arbitrary: state and state".

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.