[isabelle] inductive_set even ...
I am trying to work out the /even/ example for inductively defined sets
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:
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