Dear All,
this refers to 3fbcfa911863.
If I use the proof recording, processing of the following theory takes
infinite time:
theory Problem
imports Main
begin
lemma "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
apply (simp add: fun_eq_iff list_all2_def list_all_iff
Lifting.invariant_def Ball_def)
apply (intro allI)
apply (induct_tac rule: list_induct2')
apply simp_all
apply metis
done
end
But if I change the last step from metis to fastforce, the theory goes
through.
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]
theories "$ISABELLE_HOME/src/HOL/Problem"
Does anybody have an idea why this is happening?
Thanks,
Ondrej
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
