--- 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 &