# HG changeset patch
# User paulson
# Date 1030612536 -7200
# Node ID f76237c2be75cbb351684516c423f0cebce7b0dc
# Parent  fcdbd6cf5f9f444b07f83fb343a34a73cf3f8e81
fixed a name clash

diff -r fcdbd6cf5f9f -r f76237c2be75 src/ZF/Constructible/AC_in_L.thy
--- a/src/ZF/Constructible/AC_in_L.thy	Wed Aug 28 15:27:43 2002 +0200
+++ b/src/ZF/Constructible/AC_in_L.thy	Thu Aug 29 11:15:36 2002 +0200
@@ -432,7 +432,7 @@
 done
 
 
-lemma (in Nat_Times_Nat) well_ord_L_new_r:
+lemma (in Nat_Times_Nat) well_ord_L_succ_r:
     "[|Ord(i); well_ord(Lset(i), r); r \<subseteq> Lset(i) * Lset(i)|]
      ==> well_ord(Lset(succ(i)), L_succ_r(fn,r,i))"
 apply (rule well_ordI [OF wf_imp_wf_on])
@@ -496,13 +496,13 @@
 lemma (in Nat_Times_Nat) L_r_type:
     "Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)"
 apply (induct i rule: trans_induct3_rule)
-  apply (simp_all add: L_succ_r_type well_ord_L_new_r rlimit_def, blast) 
+  apply (simp_all add: L_succ_r_type well_ord_L_succ_r rlimit_def, blast) 
 done
 
 lemma (in Nat_Times_Nat) well_ord_L_r:
     "Ord(i) ==> well_ord(Lset(i), L_r(fn,i))"
 apply (induct i rule: trans_induct3_rule)
-apply (simp_all add: well_ord0 L_r_type well_ord_L_new_r well_ord_rlimit ltD)
+apply (simp_all add: well_ord0 L_r_type well_ord_L_succ_r well_ord_rlimit ltD)
 done
 
 lemma well_ord_L_r: