doc-src/TutorialI/Documents/Documents.thy

   following specifies an Isabelle symbol for the new operator:
 *}
 
 (*<*)
 hide const xor
-ML_setup {* Context.>> (Theory.add_path "version1") *}
+setup {* Theory.add_path "version1" *}
 (*>*)
 constdefs
   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
   "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 (*<*)

   consider the following hybrid declaration of @{text xor}:
 *}
 
 (*<*)
 hide const xor
-ML_setup {* Context.>> (Theory.add_path "version2") *}
+setup {* Theory.add_path "version2" *}
 (*>*)
 constdefs
   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
   "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"