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