[isabelle-dev] problem with the proof recording
kuncar at in.tum.de
Tue Aug 13 18:23:00 CEST 2013
this refers to 3fbcfa911863.
If I use the proof recording, processing of the following theory takes
lemma "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
apply (simp add: fun_eq_iff list_all2_def list_all_iff
apply (intro allI)
apply (induct_tac rule: list_induct2')
But if I change the last step from metis to fastforce, the theory goes
The problem doesn't happen if the theory is checked in jEdit, but it
happens when processed from the command line, e.g. by using this session:
session "HOL-Problem" = "HOL-Proofs" +
options [document = false]
Does anybody have an idea why this is happening?
More information about the isabelle-dev