[isabelle-dev] problem with the proof recording

Ondřej Kunčar kuncar at in.tum.de
Tue Aug 13 18:23:00 CEST 2013

Dear All,
this refers to 3fbcfa911863.

If I use the proof recording, processing of the following theory takes 
infinite time:

theory Problem
imports Main

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


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]
   theories "$ISABELLE_HOME/src/HOL/Problem"

Does anybody have an idea why this is happening?


More information about the isabelle-dev mailing list