diff -r e6a18808873c -r 5aa8e5e770a8 doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Thu Aug 26 21:04:22 2010 +0200 +++ b/doc-src/TutorialI/Documents/Documents.thy Fri Aug 27 00:02:32 2010 +0200 @@ -144,7 +144,7 @@ definition xor :: "bool \ bool \ bool" (infixl "\" 60) where "A \ B \ (A \ \ B) \ (\ A \ B)" (*<*) -local +setup {* Sign.local_path *} (*>*) text {* @@ -169,7 +169,7 @@ notation (xsymbols) xor (infixl "\\" 60) (*<*) -local +setup {* Sign.local_path *} (*>*) text {*\noindent