src/Pure/Examples/First_Order_Logic.thy

 subsection \<open>Abstract syntax\<close>
 
 typedecl i
 typedecl o
 
-judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
+judgment Trueprop :: "o \<Rightarrow> prop"  (\<open>_\<close> 5)
 
 
 subsection \<open>Propositional logic\<close>
 
-axiomatization false :: o  ("\<bottom>")
+axiomatization false :: o  (\<open>\<bottom>\<close>)
   where falseE [elim]: "\<bottom> \<Longrightarrow> A"
 
 
-axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr \<open>\<longrightarrow>\<close> 25)
   where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
     and mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
 
 
-axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
+axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr \<open>\<and>\<close> 35)
   where conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
     and conjD1: "A \<and> B \<Longrightarrow> A"
     and conjD2: "A \<and> B \<Longrightarrow> B"
 
 theorem conjE [elim]:

   from \<open>A \<and> B\<close> show B
     by (rule conjD2)
 qed
 
 
-axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
+axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr \<open>\<or>\<close> 30)
   where disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
     and disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
     and disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
 
 
-definition true :: o  ("\<top>")
+definition true :: o  (\<open>\<top>\<close>)
   where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
 
 theorem trueI [intro]: \<top>
   unfolding true_def ..
 
 
-definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
+definition not :: "o \<Rightarrow> o"  (\<open>\<not> _\<close> [40] 40)
   where "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
 
 theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
   unfolding not_def ..
 

   then have \<bottom> ..
   then show B ..
 qed
 
 
-definition iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longleftrightarrow>" 25)
+definition iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr \<open>\<longleftrightarrow>\<close> 25)
   where "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
 
 theorem iffI [intro]:
   assumes "A \<Longrightarrow> B"
     and "B \<Longrightarrow> A"

 qed
 
 
 subsection \<open>Equality\<close>
 
-axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infixl "=" 50)
+axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infixl \<open>=\<close> 50)
   where refl [intro]: "x = x"
     and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
 
 theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
   by (rule subst)

 qed
 
 
 subsection \<open>Quantifiers\<close>
 
-axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
+axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder \<open>\<forall>\<close> 10)
   where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
     and allD [dest]: "\<forall>x. P x \<Longrightarrow> P a"
 
-axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
+axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder \<open>\<exists>\<close> 10)
   where exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
     and exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
 
 
 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"