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 \ bool \ bool" (infixl "\" 60) @@ -164,7 +164,7 @@ (*<*) hide const xor -ML_setup {* Context.>> (Theory.add_path "version2") *} +setup {* Theory.add_path "version2" *} (*>*) constdefs xor :: "bool \ bool \ bool" (infixl "[+]\" 60)