1.1 --- a/doc-src/TutorialI/Documents/Documents.thy	Thu Aug 26 21:04:22 2010 +0200
     1.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Fri Aug 27 00:02:32 2010 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4  definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
     1.5  where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
     1.6  (*<*)
     1.7 -local
     1.8 +setup {* Sign.local_path *}
     1.9  (*>*)
    1.10  
    1.11  text {*
    1.12 @@ -169,7 +169,7 @@
    1.13  
    1.14  notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
    1.15  (*<*)
    1.16 -local
    1.17 +setup {* Sign.local_path *}
    1.18  (*>*)
    1.19  
    1.20  text {*\noindent

     2.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Thu Aug 26 21:04:22 2010 +0200
     2.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Fri Aug 27 00:02:32 2010 +0200
     2.3 @@ -168,6 +168,19 @@
     2.4  \isacommand{definition}\isamarkupfalse%
     2.5  \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
     2.6  \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
     2.7 +\isadelimML
     2.8 +%
     2.9 +\endisadelimML
    2.10 +%
    2.11 +\isatagML
    2.12 +%
    2.13 +\endisatagML
    2.14 +{\isafoldML}%
    2.15 +%
    2.16 +\isadelimML
    2.17 +%
    2.18 +\endisadelimML
    2.19 +%
    2.20  \begin{isamarkuptext}%
    2.21  \noindent The X-Symbol package within Proof~General provides several
    2.22    input methods to enter \isa{{\isasymoplus}} in the text.  If all fails one may
    2.23 @@ -200,6 +213,19 @@
    2.24  \isanewline
    2.25  \isacommand{notation}\isamarkupfalse%
    2.26  \ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}%
    2.27 +\isadelimML
    2.28 +%
    2.29 +\endisadelimML
    2.30 +%
    2.31 +\isatagML
    2.32 +%
    2.33 +\endisatagML
    2.34 +{\isafoldML}%
    2.35 +%
    2.36 +\isadelimML
    2.37 +%
    2.38 +\endisadelimML
    2.39 +%
    2.40  \begin{isamarkuptext}%
    2.41  \noindent
    2.42  The \commdx{notation} command associates a mixfix