doc-src/TutorialI/Documents/document/Documents.tex
changeset 38765 5aa8e5e770a8
parent 30649 57753e0ec1d4
child 40406 313a24b66a8d
     1.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Thu Aug 26 21:04:22 2010 +0200
     1.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Fri Aug 27 00:02:32 2010 +0200
     1.3 @@ -168,6 +168,19 @@
     1.4  \isacommand{definition}\isamarkupfalse%
     1.5  \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
     1.6  \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
     1.7 +\isadelimML
     1.8 +%
     1.9 +\endisadelimML
    1.10 +%
    1.11 +\isatagML
    1.12 +%
    1.13 +\endisatagML
    1.14 +{\isafoldML}%
    1.15 +%
    1.16 +\isadelimML
    1.17 +%
    1.18 +\endisadelimML
    1.19 +%
    1.20  \begin{isamarkuptext}%
    1.21  \noindent The X-Symbol package within Proof~General provides several
    1.22    input methods to enter \isa{{\isasymoplus}} in the text.  If all fails one may
    1.23 @@ -200,6 +213,19 @@
    1.24  \isanewline
    1.25  \isacommand{notation}\isamarkupfalse%
    1.26  \ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}%
    1.27 +\isadelimML
    1.28 +%
    1.29 +\endisadelimML
    1.30 +%
    1.31 +\isatagML
    1.32 +%
    1.33 +\endisatagML
    1.34 +{\isafoldML}%
    1.35 +%
    1.36 +\isadelimML
    1.37 +%
    1.38 +\endisadelimML
    1.39 +%
    1.40  \begin{isamarkuptext}%
    1.41  \noindent
    1.42  The \commdx{notation} command associates a mixfix