Re: [isabelle] inductive_set even ...
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and