# HG changeset patch # User wenzelm # Date 1584549867 -3600 # Node ID 1005c50b2750acdb63c258b009b73ed78d4f8580 # Parent 9a29e883a93471da7d434d637e6c402fb27f2d12 prefer strict qualification (default for 'interpretation', see 461ee3e49ad3) as proposed by Pedro Sánchez Terraf; diff -r 9a29e883a934 -r 1005c50b2750 src/ZF/Constructible/AC_in_L.thy --- a/src/ZF/Constructible/AC_in_L.thy Wed Mar 18 17:29:20 2020 +0100 +++ b/src/ZF/Constructible/AC_in_L.thy Wed Mar 18 17:44:27 2020 +0100 @@ -460,7 +460,7 @@ apply (blast dest!: well_ord_L_r intro: well_ord_subset) done -interpretation L?: M_basic L by (rule M_basic_L) +interpretation L: M_basic L by (rule M_basic_L) theorem "\x[L]. \r. wellordered(L,x,r)" proof @@ -469,7 +469,7 @@ then obtain r where "well_ord(x,r)" by (blast dest: L_implies_AC) thus "\r. wellordered(L,x,r)" - by (blast intro: well_ord_imp_relativized) + by (blast intro: L.well_ord_imp_relativized) qed text\In order to prove \<^term>\ \r[L]. wellordered(L,x,r)\, it's necessary to know diff -r 9a29e883a934 -r 1005c50b2750 src/ZF/Constructible/DPow_absolute.thy --- a/src/ZF/Constructible/DPow_absolute.thy Wed Mar 18 17:29:20 2020 +0100 +++ b/src/ZF/Constructible/DPow_absolute.thy Wed Mar 18 17:44:27 2020 +0100 @@ -581,7 +581,7 @@ ==> transrec_replacement(L, \x f u. \r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & big_union(L, r, u), j)" -apply (rule transrec_replacementI, assumption) +apply (rule L.transrec_replacementI, assumption) apply (unfold transrec_body_def) apply (rule strong_replacementI) apply (rule_tac u="{j,B,Memrel(eclose({j}))}" diff -r 9a29e883a934 -r 1005c50b2750 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Wed Mar 18 17:29:20 2020 +0100 +++ b/src/ZF/Constructible/L_axioms.thy Wed Mar 18 17:44:27 2020 +0100 @@ -110,7 +110,7 @@ apply (rule Union_ax) done -interpretation L?: M_trivial L by (rule M_trivial_L) +interpretation L: M_trivial L by (rule M_trivial_L) (* Replaces the following declarations... lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L] diff -r 9a29e883a934 -r 1005c50b2750 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Wed Mar 18 17:29:20 2020 +0100 +++ b/src/ZF/Constructible/Rec_Separation.thy Wed Mar 18 17:44:27 2020 +0100 @@ -184,7 +184,7 @@ theorem M_trancl_L: "M_trancl(L)" by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L]) -interpretation L?: M_trancl L by (rule M_trancl_L) +interpretation L: M_trancl L by (rule M_trancl_L) subsection\\<^term>\L\ is Closed Under the Operator \<^term>\list\\ @@ -371,7 +371,7 @@ apply (rule M_datatypes_axioms_L) done -interpretation L?: M_datatypes L by (rule M_datatypes_L) +interpretation L: M_datatypes L by (rule M_datatypes_L) subsection\\<^term>\L\ is Closed Under the Operator \<^term>\eclose\\ @@ -434,7 +434,7 @@ apply (rule M_eclose_axioms_L) done -interpretation L?: M_eclose L by (rule M_eclose_L) +interpretation L: M_eclose L by (rule M_eclose_L) end diff -r 9a29e883a934 -r 1005c50b2750 src/ZF/Constructible/Satisfies_absolute.thy --- a/src/ZF/Constructible/Satisfies_absolute.thy Wed Mar 18 17:29:20 2020 +0100 +++ b/src/ZF/Constructible/Satisfies_absolute.thy Wed Mar 18 17:44:27 2020 +0100 @@ -961,11 +961,11 @@ lemma formula_rec_replacement: \ \For the \<^term>\transrec\\ "[|n \ nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)" -apply (rule transrec_replacementI, simp add: nat_into_M) +apply (rule L.transrec_replacementI, simp add: L.nat_into_M) apply (rule strong_replacementI) apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}" in gen_separation_multi [OF formula_rec_replacement_Reflects], - auto simp add: nat_into_M) + auto simp add: L.nat_into_M) apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI) apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+ done diff -r 9a29e883a934 -r 1005c50b2750 src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Wed Mar 18 17:29:20 2020 +0100 +++ b/src/ZF/Constructible/Separation.thy Wed Mar 18 17:44:27 2020 +0100 @@ -304,7 +304,7 @@ theorem M_basic_L: " M_basic(L)" by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L]) -interpretation L?: M_basic L by (rule M_basic_L) +interpretation L: M_basic L by (rule M_basic_L) end