# HG changeset patch # User kleing # Date 976703088 -3600 # Node ID fcd8d4e7d75869ef3c51d9f0c15cabdb5bba205e # Parent a196b944569b6d5bcd44d5036a493cff8d691648 fixed iter_wf proof diff -r a196b944569b -r fcd8d4e7d758 src/HOL/MicroJava/BV/Kildall.thy --- a/src/HOL/MicroJava/BV/Kildall.thy Wed Dec 13 10:34:45 2000 +0100 +++ b/src/HOL/MicroJava/BV/Kildall.thy Wed Dec 13 11:24:48 2000 +0100 @@ -212,10 +212,10 @@ val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter"; in goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf)); -by (REPEAT(rtac wf_same_fstI 1)); +by (REPEAT(rtac wf_same_fst 1)); by (split_all_tac 1); by (asm_full_simp_tac (simpset() addsimps [thm "lesssub_def"]) 1); -by (REPEAT(rtac wf_same_fstI 1)); +by (REPEAT(rtac wf_same_fst 1)); by (rtac wf_lex_prod 1); by (rtac wf_finite_psubset 2); by (Clarify_tac 1); @@ -265,7 +265,6 @@ end *} - lemma iter_induct: "(!!A r f step succs ss w. (!p. p = (@ p. p : w) & w ~= {} & semilat(A,r,f) & acc r &