doc-src/TutorialI/Documents/Documents.thy

   Replacing our previous definition of @{text xor} by the
   following specifies an Isabelle symbol for the new operator:
 *}
 
 (*<*)
-hide const xor
+hide_const xor
 setup {* Sign.add_path "version1" *}
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
 where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 (*<*)

   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
   consider the following hybrid declaration of @{text xor}:
 *}
 
 (*<*)
-hide const xor
+hide_const xor
 setup {* Sign.add_path "version2" *}
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
 where "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"