# HG changeset patch
# User wenzelm
# Date 1169240885 -3600
# Node ID 88be1b7775c8fb49e71476b6d727afc904a217ab
# Parent  7ee0529c56741a4b1fb39ac75e785f930f8be3c1
tuned;

diff -r 7ee0529c5674 -r 88be1b7775c8 doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Fri Jan 19 22:08:04 2007 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy	Fri Jan 19 22:08:05 2007 +0100
@@ -140,7 +140,7 @@
 
 (*<*)
 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)
@@ -164,7 +164,7 @@
 
 (*<*)
 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)