src/Doc/Tutorial/Documents/Documents.thy

   Infix declarations\index{infix annotations} provide a useful special
   case of mixfixes.  The following example of the exclusive-or
   operation on boolean values illustrates typical infix declarations.
 \<close>
 
-definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl \<open>[+]\<close> 60)
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]" 60)
 where "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 
 text \<open>
   \noindent Now \<open>xor A B\<close> and \<open>A [+] B\<close> refer to the
   same expression internally.  Any curried function with at least two

 
 (*<*)
 hide_const xor
 setup \<open>Sign.add_path "version1"\<close>
 (*>*)
-definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl \<open>\<oplus>\<close> 60)
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
 where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 (*<*)
 setup \<open>Sign.local_path\<close>
 (*>*)
 

 
 (*<*)
 hide_const xor
 setup \<open>Sign.add_path "version2"\<close>
 (*>*)
-definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl \<open>[+]\<ignore>\<close> 60)
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
 where "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 
-notation (xsymbols) xor (infixl \<open>\<oplus>\<ignore>\<close> 60)
+notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
 (*<*)
 setup \<open>Sign.local_path\<close>
 (*>*)
 
 text \<open>\noindent

   priorities --- just some literal syntax.  The following example
   associates common symbols with the constructors of a datatype.
 \<close>
 
 datatype currency =
-    Euro nat    (\<open>\<euro>\<close>)
-  | Pounds nat  (\<open>\<pounds>\<close>)
-  | Yen nat     (\<open>\<yen>\<close>)
-  | Dollar nat  (\<open>$\<close>)
+    Euro nat    ("\<euro>")
+  | Pounds nat  ("\<pounds>")
+  | Yen nat     ("\<yen>")
+  | Dollar nat  ("$")
 
 text \<open>
   \noindent Here the mixfix annotations on the rightmost column happen
   to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
   \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,.  Recall

 A typical use of abbreviations is to introduce relational notation for
 membership in a set of pairs, replacing \<open>(x, y) \<in> sim\<close> by
 \<open>x \<approx> y\<close>. We assume that a constant \<open>sim\<close> of type
 \<^typ>\<open>('a \<times> 'a) set\<close> has been introduced at this point.\<close>
 (*<*)consts sim :: "('a \<times> 'a) set"(*>*)
-abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"   (infix \<open>\<approx>\<close> 50)
+abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"   (infix "\<approx>" 50)
 where "x \<approx> y  \<equiv>  (x, y) \<in> sim"
 
 text \<open>\noindent The given meta-equality is used as a rewrite rule
 after parsing (replacing \mbox{\<^prop>\<open>x \<approx> y\<close>} by \<open>(x,y) \<in>
 sim\<close>) and before printing (turning \<open>(x,y) \<in> sim\<close> back into

 provide variant versions of fundamental relational expressions, such
 as \<open>\<noteq>\<close> for negated equalities.  The following declaration
 stems from Isabelle/HOL itself:
 \<close>
 
-abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl \<open>~=\<ignore>\<close> 50)
+abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "~=\<ignore>" 50)
 where "x ~=\<ignore> y  \<equiv>  \<not> (x = y)"
 
-notation (xsymbols) not_equal (infix \<open>\<noteq>\<ignore>\<close> 50)
+notation (xsymbols) not_equal (infix "\<noteq>\<ignore>" 50)
 
 text \<open>\noindent The notation \<open>\<noteq>\<close> is introduced separately to restrict it
 to the \emph{xsymbols} mode.
 
 Abbreviations are appropriate when the defined concept is a