[isabelle] inductive_set even ...


I am trying to work out the /even/ example for inductively defined sets using Isabelle2007.
I have also turned on the trace_simp variable.

While trying to discharge the first lemma:
   lemma two_times_even[intro!]: "2*k \<in> even"
the trace displays the following:

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

Any idea what the "??.unknown" is? I cannot recall seeing it with the 05 version but I may be wrong.


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