Re: [isabelle] inductive_set even ...



   [1]Adding rewrite rule "??.unknown":
   2 * n : even == True

Any idea what the "??.unknown" is?

The rule comes from the induction hypothesis (the premise of the second subgoal), and it is automatically used to simplify the induction step. Since it is just local and does not have a proper name (like a lemma), it gets some funny internal name. I am not sure if Isabelle2005 displayed the names like this but it certainly behaved in the same way.

Alex





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