# HG changeset patch
# User wenzelm
# Date 1282860152 -7200
# Node ID 5aa8e5e770a87347e893802d0dbb00eb6c0da5b2
# Parent  e6a18808873cb79e455dbc7d473afee28afb3ea1
eliminated old 'local' command;

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 \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
 where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 (*<*)
-local
+setup {* Sign.local_path *}
 (*>*)
 
 text {*
@@ -169,7 +169,7 @@
 
 notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
 (*<*)
-local
+setup {* Sign.local_path *}
 (*>*)
 
 text {*\noindent
diff -r e6a18808873c -r 5aa8e5e770a8 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Thu Aug 26 21:04:22 2010 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Fri Aug 27 00:02:32 2010 +0200
@@ -168,6 +168,19 @@
 \isacommand{definition}\isamarkupfalse%
 \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
 \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
 \begin{isamarkuptext}%
 \noindent The X-Symbol package within Proof~General provides several
   input methods to enter \isa{{\isasymoplus}} in the text.  If all fails one may
@@ -200,6 +213,19 @@
 \isanewline
 \isacommand{notation}\isamarkupfalse%
 \ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
 \begin{isamarkuptext}%
 \noindent
 The \commdx{notation} command associates a mixfix