src/ZF/Constructible/L_axioms.thy

 
 section \<open>The ZF Axioms (Except Separation) in L\<close>
 
 theory L_axioms imports Formula Relative Reflection MetaExists begin
 
-text \<open>The class L satisfies the premises of locale @{text M_trivial}\<close>
+text \<open>The class L satisfies the premises of locale \<open>M_trivial\<close>\<close>
 
 lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
 apply (insert Transset_Lset)
 apply (simp add: Transset_def L_def, blast)
 done

 apply (frule LReplace_in_L, assumption+, clarify)
 apply (rule_tac x=Y in rexI)
 apply (simp_all add: Replace_iff univalent_def, blast)
 done
 
-subsection\<open>Instantiating the locale @{text M_trivial}\<close>
+subsection\<open>Instantiating the locale \<open>M_trivial\<close>\<close>
 text\<open>No instances of Separation yet.\<close>
 
 lemma Lset_mono_le: "mono_le_subset(Lset)"
 by (simp add: mono_le_subset_def le_imp_subset Lset_mono)
 

 declare rall_abs [simp]
 declare rex_abs [simp]
 ...and dozens of similar ones.
 *)
 
-subsection\<open>Instantiation of the locale @{text reflection}\<close>
+subsection\<open>Instantiation of the locale \<open>reflection\<close>\<close>
 
 text\<open>instances of locale constants\<close>
 
 definition
   L_F0 :: "[i=>o,i] => i" where

 apply (unfold rall_def)
 apply (intro Imp_reflection All_reflection, assumption)
 done
 
 text\<open>This version handles an alternative form of the bounded quantifier
-      in the second argument of @{text REFLECTS}.\<close>
+      in the second argument of \<open>REFLECTS\<close>.\<close>
 theorem Rex_reflection':
      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
       ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[##Lset(a)]. Q(a,x,z)]"
 apply (unfold setclass_def rex_def)
 apply (erule Rex_reflection [unfolded rex_def Bex_def]) 

 done
 
 
 subsubsection\<open>Variants of Satisfaction Definitions for Ordinals, etc.\<close>
 
-text\<open>The @{text sats} theorems below are standard versions of the ones proved
-in theory @{text Formula}.  They relate elements of type @{term formula} to
+text\<open>The \<open>sats\<close> theorems below are standard versions of the ones proved
+in theory \<open>Formula\<close>.  They relate elements of type @{term formula} to
 relativized concepts such as @{term subset} or @{term ordinal} rather than to
 real concepts such as @{term Ord}.  Now that we have instantiated the locale
-@{text M_trivial}, we no longer require the earlier versions.\<close>
+\<open>M_trivial\<close>, we no longer require the earlier versions.\<close>
 
 lemma sats_subset_fm':
    "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, subset_fm(x,y), env) \<longleftrightarrow> subset(##A, nth(x,env), nth(y,env))"
 by (simp add: subset_fm_def Relative.subset_def)