*** empty log message ***
authorwenzelm
Mon Oct 08 12:28:43 2001 +0200 (2001-10-08)
changeset 11708d27253c4594f
parent 11707 6c45813c2db1
child 11709 f4d287d924bb
*** empty log message ***
doc-src/TutorialI/Inductive/document/AB.tex
doc-src/TutorialI/Inductive/document/Advanced.tex
doc-src/TutorialI/Inductive/document/Even.tex
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/Misc/document/appendix.tex
doc-src/TutorialI/Misc/document/case_exprs.tex
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Types/document/Numbers.tex
doc-src/TutorialI/Types/document/Pairs.tex
doc-src/TutorialI/isabellesym.sty
     1.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Mon Oct 08 12:27:19 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Mon Oct 08 12:28:43 2001 +0200
     1.3 @@ -95,13 +95,13 @@
     1.4  1 on our way from 0 to 2. Formally, we appeal to the following discrete
     1.5  intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
     1.6  \begin{isabelle}%
     1.7 -\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
     1.8 +\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ i\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ Numeral{\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
     1.9  \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
    1.10  \end{isabelle}
    1.11  where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
    1.12  \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See
    1.13  Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
    1.14 -syntax.}, and \isa{{\isacharhash}{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}).
    1.15 +syntax.}, and \isa{{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}).
    1.16  
    1.17  First we show that our specific function, the difference between the
    1.18  numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
    1.19 @@ -112,7 +112,7 @@
    1.20  \end{isamarkuptext}%
    1.21  \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
    1.22  \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
    1.23 -\ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
    1.24 +\ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ Numeral{\isadigit{1}}{\isachardoublequote}%
    1.25  \begin{isamarkuptxt}%
    1.26  \noindent
    1.27  The lemma is a bit hard to read because of the coercion function
    1.28 @@ -128,7 +128,7 @@
    1.29  \end{isamarkuptxt}%
    1.30  \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline
    1.31  \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
    1.32 -\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
    1.33 +\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
    1.34  \begin{isamarkuptext}%
    1.35  Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:%
    1.36  \end{isamarkuptext}%
    1.37 @@ -141,7 +141,7 @@
    1.38  instantiated appropriately and with its first premise disposed of by lemma
    1.39  \isa{step{\isadigit{1}}}:%
    1.40  \end{isamarkuptxt}%
    1.41 -\isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline
    1.42 +\isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}Numeral{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline
    1.43  \isacommand{by}\ force%
    1.44  \begin{isamarkuptext}%
    1.45  \noindent
     2.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Oct 08 12:27:19 2001 +0200
     2.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Oct 08 12:28:43 2001 +0200
     2.3 @@ -90,9 +90,9 @@
     2.4  \isanewline
     2.5  \isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
     2.6  \isacommand{primrec}\isanewline
     2.7 -{\isachardoublequote}integer{\isacharunderscore}arity\ {\isacharparenleft}Number\ n{\isacharparenright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharhash}{\isadigit{0}}{\isachardoublequote}\isanewline
     2.8 -{\isachardoublequote}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}\isanewline
     2.9 -{\isachardoublequote}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharhash}{\isadigit{2}}{\isachardoublequote}\isanewline
    2.10 +{\isachardoublequote}integer{\isacharunderscore}arity\ {\isacharparenleft}Number\ n{\isacharparenright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
    2.11 +{\isachardoublequote}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
    2.12 +{\isachardoublequote}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{2}}{\isachardoublequote}\isanewline
    2.13  \isanewline
    2.14  \isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
    2.15  \isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
     3.1 --- a/doc-src/TutorialI/Inductive/document/Even.tex	Mon Oct 08 12:27:19 2001 +0200
     3.2 +++ b/doc-src/TutorialI/Inductive/document/Even.tex	Mon Oct 08 12:28:43 2001 +0200
     3.3 @@ -28,14 +28,14 @@
     3.4  
     3.5  Our first lemma states that numbers of the form $2\times k$ are even.%
     3.6  \end{isamarkuptext}%
     3.7 -\isacommand{lemma}\ two{\isacharunderscore}times{\isacharunderscore}even{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharhash}{\isadigit{2}}{\isacharasterisk}k\ {\isasymin}\ even{\isachardoublequote}\isanewline
     3.8 +\isacommand{lemma}\ two{\isacharunderscore}times{\isacharunderscore}even{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isadigit{2}}{\isacharasterisk}k\ {\isasymin}\ even{\isachardoublequote}\isanewline
     3.9  \isacommand{apply}\ {\isacharparenleft}induct\ {\isachardoublequote}k{\isachardoublequote}{\isacharparenright}%
    3.10  \begin{isamarkuptxt}%
    3.11  The first step is induction on the natural number \isa{k}, which leaves
    3.12  two subgoals:
    3.13  \begin{isabelle}%
    3.14 -\ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline
    3.15 -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even%
    3.16 +\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline
    3.17 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even%
    3.18  \end{isabelle}
    3.19  Here \isa{auto} simplifies both subgoals so that they match the introduction
    3.20  rules, which then are applied automatically.%
    3.21 @@ -48,29 +48,29 @@
    3.22  this equivalence is trivial using the lemma just proved, whose \isa{intro!}
    3.23  attribute ensures it will be applied automatically.%
    3.24  \end{isamarkuptext}%
    3.25 -\isacommand{lemma}\ dvd{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequote}{\isacharhash}{\isadigit{2}}\ dvd\ n\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline
    3.26 +\isacommand{lemma}\ dvd{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequote}{\isadigit{2}}\ dvd\ n\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline
    3.27  \isacommand{by}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}%
    3.28  \begin{isamarkuptext}%
    3.29  our first rule induction!%
    3.30  \end{isamarkuptext}%
    3.31 -\isacommand{lemma}\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ n{\isachardoublequote}\isanewline
    3.32 +\isacommand{lemma}\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ n{\isachardoublequote}\isanewline
    3.33  \isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}%
    3.34  \begin{isamarkuptxt}%
    3.35  \begin{isabelle}%
    3.36 -\ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
    3.37 -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isacharhash}{\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    3.38 +\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
    3.39 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    3.40  \end{isabelle}%
    3.41  \end{isamarkuptxt}%
    3.42  \isacommand{apply}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}%
    3.43  \begin{isamarkuptxt}%
    3.44  \begin{isabelle}%
    3.45 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k%
    3.46 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k%
    3.47  \end{isabelle}%
    3.48  \end{isamarkuptxt}%
    3.49  \isacommand{apply}\ clarify%
    3.50  \begin{isamarkuptxt}%
    3.51  \begin{isabelle}%
    3.52 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ ka%
    3.53 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ ka%
    3.54  \end{isabelle}%
    3.55  \end{isamarkuptxt}%
    3.56  \isacommand{apply}\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}Suc\ k{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharcomma}\ simp{\isacharparenright}\isanewline
    3.57 @@ -78,7 +78,7 @@
    3.58  \begin{isamarkuptext}%
    3.59  no iff-attribute because we don't always want to use it%
    3.60  \end{isamarkuptext}%
    3.61 -\isacommand{theorem}\ even{\isacharunderscore}iff{\isacharunderscore}dvd{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}n\ {\isasymin}\ even{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}\ dvd\ n{\isacharparenright}{\isachardoublequote}\isanewline
    3.62 +\isacommand{theorem}\ even{\isacharunderscore}iff{\isacharunderscore}dvd{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}n\ {\isasymin}\ even{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{2}}\ dvd\ n{\isacharparenright}{\isachardoublequote}\isanewline
    3.63  \isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharcolon}\ dvd{\isacharunderscore}imp{\isacharunderscore}even\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}%
    3.64  \begin{isamarkuptext}%
    3.65  this result ISN'T inductive...%
    3.66 @@ -95,12 +95,12 @@
    3.67  \begin{isamarkuptext}%
    3.68  ...so we need an inductive lemma...%
    3.69  \end{isamarkuptext}%
    3.70 -\isacommand{lemma}\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n{\isacharminus}{\isacharhash}{\isadigit{2}}\ {\isasymin}\ even{\isachardoublequote}\isanewline
    3.71 +\isacommand{lemma}\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even{\isachardoublequote}\isanewline
    3.72  \isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}%
    3.73  \begin{isamarkuptxt}%
    3.74  \begin{isabelle}%
    3.75 -\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even\isanewline
    3.76 -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isacharhash}{\isadigit{2}}\ {\isasymin}\ even%
    3.77 +\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even\isanewline
    3.78 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even%
    3.79  \end{isabelle}%
    3.80  \end{isamarkuptxt}%
    3.81  \isacommand{apply}\ auto\isanewline
     4.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Oct 08 12:27:19 2001 +0200
     4.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Oct 08 12:28:43 2001 +0200
     4.3 @@ -171,7 +171,7 @@
     4.4  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
     4.5  \end{isabelle}
     4.6  After stripping the \isa{{\isasymforall}i}, the proof continues with a case
     4.7 -distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on
     4.8 +distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}} is trivial and we focus on
     4.9  the other case:%
    4.10  \end{isamarkuptxt}%
    4.11  \isacommand{apply}{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline
     5.1 --- a/doc-src/TutorialI/Misc/document/appendix.tex	Mon Oct 08 12:27:19 2001 +0200
     5.2 +++ b/doc-src/TutorialI/Misc/document/appendix.tex	Mon Oct 08 12:28:43 2001 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4  \begin{tabular}{lll}
     5.5  Constant & Type & Syntax \\
     5.6  \hline
     5.7 -\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
     5.8 +\isa{{\isadigit{0}}{\isasymColon}{\isacharprime}a} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
     5.9  \isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
    5.10  \isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} &  (infixl 65) \\
    5.11  \isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
     6.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Oct 08 12:27:19 2001 +0200
     6.2 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Oct 08 12:28:43 2001 +0200
     6.3 @@ -10,9 +10,9 @@
     6.4  HOL also features \isa{case}-expressions for analyzing
     6.5  elements of a datatype. For example,
     6.6  \begin{isabelle}%
     6.7 -\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
     6.8 +\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
     6.9  \end{isabelle}
    6.10 -evaluates to \isa{{\isadigit{1}}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if 
    6.11 +evaluates to \isa{{\isadigit{1}}{\isasymColon}{\isacharprime}a} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if 
    6.12  \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of
    6.13  the same type, it follows that \isa{y} is of type \isa{nat} and hence
    6.14  that \isa{xs} is of type \isa{nat\ list}.)
    6.15 @@ -41,7 +41,7 @@
    6.16  \end{isabelle}
    6.17  write
    6.18  \begin{isabelle}%
    6.19 -\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\isanewline
    6.20 +\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a\isanewline
    6.21  \isaindent{\ \ \ \ \ }{\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y%
    6.22  \end{isabelle}
    6.23  
     7.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Oct 08 12:27:19 2001 +0200
     7.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon Oct 08 12:28:43 2001 +0200
     7.3 @@ -30,13 +30,13 @@
     7.4  \sdx{div}, \sdx{mod}, \cdx{min} and
     7.5  \cdx{max} are predefined, as are the relations
     7.6  \indexboldpos{\isasymle}{$HOL2arithrel} and
     7.7 -\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
     7.8 +\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}} if
     7.9  \isa{m\ {\isacharless}\ n}. There is even a least number operation
    7.10 -\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}. 
    7.11 +\sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}}. 
    7.12  \REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
    7.13   The following needs changing with our new system of numbers.}
    7.14 -Note that \isa{{\isadigit{1}}}
    7.15 -and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
    7.16 +Note that \isa{{\isadigit{1}}{\isasymColon}{\isacharprime}a}
    7.17 +and \isa{{\isadigit{2}}{\isasymColon}{\isacharprime}a} are available as abbreviations for the corresponding
    7.18  \isa{Suc}-expressions. If you need the full set of numerals,
    7.19  see~\S\ref{sec:numerals}.
    7.20  
    7.21 @@ -47,10 +47,10 @@
    7.22    \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
    7.23    \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
    7.24    not just for natural numbers but at other types as well.
    7.25 -  For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x},
    7.26 +  For example, given the goal \isa{x\ {\isacharplus}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ x},
    7.27    there is nothing to indicate that you are talking about natural numbers.
    7.28    Hence Isabelle can only infer that \isa{x} is of some arbitrary type where
    7.29 -  \isa{{\isadigit{0}}} and \isa{{\isacharplus}} are declared. As a consequence, you will be unable
    7.30 +  \isa{{\isadigit{0}}{\isasymColon}{\isacharprime}a} and \isa{{\isacharplus}} are declared. As a consequence, you will be unable
    7.31    to prove the goal (although it may take you some time to realize what has
    7.32    happened if \isa{show{\isacharunderscore}types} is not set).  In this particular example,
    7.33    you need to include an explicit type constraint, for example
    7.34 @@ -67,14 +67,14 @@
    7.35  (a method introduced below, \S\ref{sec:Simplification}) prove 
    7.36  simple arithmetic goals automatically:%
    7.37  \end{isamarkuptext}%
    7.38 -\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
    7.39 +\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
    7.40  \begin{isamarkuptext}%
    7.41  \noindent
    7.42  For efficiency's sake, this built-in prover ignores quantified formulae,
    7.43  logical connectives, and all arithmetic operations apart from addition.
    7.44  In consequence, \isa{auto} cannot prove this slightly more complex goal:%
    7.45  \end{isamarkuptext}%
    7.46 -\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
    7.47 +\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
    7.48  \begin{isamarkuptext}%
    7.49  \noindent
    7.50  The method \methdx{arith} is more general.  It attempts to prove
    7.51 @@ -105,7 +105,7 @@
    7.52  
    7.53    Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
    7.54    role, it may fail to prove a valid formula, for example
    7.55 -  \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare.
    7.56 +  \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}}. Fortunately, such examples are rare.
    7.57  \end{warn}%
    7.58  \end{isamarkuptext}%
    7.59  \end{isabellebody}%
     8.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Mon Oct 08 12:27:19 2001 +0200
     8.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Mon Oct 08 12:28:43 2001 +0200
     8.3 @@ -9,40 +9,40 @@
     8.4  \begin{isamarkuptext}%
     8.5  numeric literals; default simprules; can re-orient%
     8.6  \end{isamarkuptext}%
     8.7 -\isacommand{lemma}\ {\isachardoublequote}{\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequote}%
     8.8 +\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequote}%
     8.9  \begin{isamarkuptxt}%
    8.10  \begin{isabelle}%
    8.11 -\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m%
    8.12 +\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m%
    8.13  \end{isabelle}%
    8.14  \end{isamarkuptxt}%
    8.15  \isacommand{oops}\isanewline
    8.16  \isanewline
    8.17  \isacommand{consts}\ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    8.18  \isacommand{recdef}\ h\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline
    8.19 -{\isachardoublequote}h\ i\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isacharequal}\ {\isacharhash}{\isadigit{3}}\ then\ {\isacharhash}{\isadigit{2}}\ else\ i{\isacharparenright}{\isachardoublequote}%
    8.20 +{\isachardoublequote}h\ i\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isacharequal}\ {\isadigit{3}}\ then\ {\isadigit{2}}\ else\ i{\isacharparenright}{\isachardoublequote}%
    8.21  \begin{isamarkuptext}%
    8.22 -\isa{h\ {\isacharhash}{\isadigit{3}}\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}}
    8.23 +\isa{h\ {\isadigit{3}}\ {\isacharequal}\ {\isadigit{2}}}
    8.24  \isa{h\ i\ {\isacharequal}\ i}%
    8.25  \end{isamarkuptext}%
    8.26  %
    8.27  \begin{isamarkuptext}%
    8.28  \begin{isabelle}%
    8.29 -{\isacharhash}{\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}%
    8.30 +Numeral{\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}%
    8.31  \end{isabelle}
    8.32  \rulename{numeral_0_eq_0}
    8.33  
    8.34  \begin{isabelle}%
    8.35 -{\isacharhash}{\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}%
    8.36 +Numeral{\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}%
    8.37  \end{isabelle}
    8.38  \rulename{numeral_1_eq_1}
    8.39  
    8.40  \begin{isabelle}%
    8.41 -{\isacharhash}{\isadigit{2}}\ {\isacharplus}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    8.42 +{\isadigit{2}}\ {\isacharplus}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    8.43  \end{isabelle}
    8.44  \rulename{add_2_eq_Suc}
    8.45  
    8.46  \begin{isabelle}%
    8.47 -n\ {\isacharplus}\ {\isacharhash}{\isadigit{2}}\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    8.48 +n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    8.49  \end{isabelle}
    8.50  \rulename{add_2_eq_Suc'}
    8.51  
    8.52 @@ -113,11 +113,11 @@
    8.53  \end{isabelle}
    8.54  \rulename{nat_diff_split}%
    8.55  \end{isamarkuptext}%
    8.56 -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n{\isacharminus}{\isacharhash}{\isadigit{2}}{\isacharparenright}{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isacharhash}{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}n\ {\isacharminus}\ {\isacharparenleft}{\isacharhash}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
    8.57 +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
    8.58  \isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
    8.59  \ %
    8.60  \isamarkupcmt{\begin{isabelle}%
    8.61 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ {\isacharhash}{\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ {\isacharhash}{\isadigit{4}}\ {\isacharplus}\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
    8.62 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ {\isadigit{4}}\ {\isacharplus}\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
    8.63  \end{isabelle}%
    8.64  }
    8.65  \isanewline
    8.66 @@ -187,22 +187,22 @@
    8.67  
    8.68  
    8.69  \begin{isabelle}%
    8.70 -{\isacharhash}{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{0}}\ {\isasymle}\ a\ mod\ b%
    8.71 +Numeral{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ Numeral{\isadigit{0}}\ {\isasymle}\ a\ mod\ b%
    8.72  \end{isabelle}
    8.73  \rulename{pos_mod_sign}
    8.74  
    8.75  \begin{isabelle}%
    8.76 -{\isacharhash}{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isacharless}\ b%
    8.77 +Numeral{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isacharless}\ b%
    8.78  \end{isabelle}
    8.79  \rulename{pos_mod_bound}
    8.80  
    8.81  \begin{isabelle}%
    8.82 -b\ {\isacharless}\ {\isacharhash}{\isadigit{0}}\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isasymle}\ {\isacharhash}{\isadigit{0}}%
    8.83 +b\ {\isacharless}\ Numeral{\isadigit{0}}\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isasymle}\ Numeral{\isadigit{0}}%
    8.84  \end{isabelle}
    8.85  \rulename{neg_mod_sign}
    8.86  
    8.87  \begin{isabelle}%
    8.88 -b\ {\isacharless}\ {\isacharhash}{\isadigit{0}}\ {\isasymLongrightarrow}\ b\ {\isacharless}\ a\ mod\ b%
    8.89 +b\ {\isacharless}\ Numeral{\isadigit{0}}\ {\isasymLongrightarrow}\ b\ {\isacharless}\ a\ mod\ b%
    8.90  \end{isabelle}
    8.91  \rulename{neg_mod_bound}
    8.92  
    8.93 @@ -227,12 +227,12 @@
    8.94  \rulename{zmod_zmult1_eq}
    8.95  
    8.96  \begin{isabelle}%
    8.97 -{\isacharhash}{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c%
    8.98 +Numeral{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c%
    8.99  \end{isabelle}
   8.100  \rulename{zdiv_zmult2_eq}
   8.101  
   8.102  \begin{isabelle}%
   8.103 -{\isacharhash}{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b%
   8.104 +Numeral{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b%
   8.105  \end{isabelle}
   8.106  \rulename{zmod_zmult2_eq}
   8.107  
   8.108 @@ -244,7 +244,7 @@
   8.109  \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline
   8.110  \isacommand{by}\ arith\isanewline
   8.111  \isanewline
   8.112 -\isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isacharhash}{\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline
   8.113 +\isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline
   8.114  \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def{\isacharparenright}%
   8.115  \begin{isamarkuptext}%
   8.116  REALS
   8.117 @@ -301,38 +301,38 @@
   8.118  \end{isabelle}
   8.119  \rulename{real_add_divide_distrib}%
   8.120  \end{isamarkuptext}%
   8.121 -\isacommand{lemma}\ {\isachardoublequote}{\isacharhash}{\isadigit{3}}{\isacharslash}{\isacharhash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isacharhash}{\isadigit{7}}{\isacharslash}{\isacharhash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline
   8.122 +\isacommand{lemma}\ {\isachardoublequote}{\isadigit{3}}{\isacharslash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isadigit{7}}{\isacharslash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline
   8.123  \isacommand{by}\ simp\ \isanewline
   8.124  \isanewline
   8.125 -\isacommand{lemma}\ {\isachardoublequote}P\ {\isacharparenleft}{\isacharparenleft}{\isacharhash}{\isadigit{3}}{\isacharslash}{\isacharhash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharhash}{\isadigit{8}}{\isacharslash}{\isacharhash}{\isadigit{1}}{\isadigit{5}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
   8.126 +\isacommand{lemma}\ {\isachardoublequote}P\ {\isacharparenleft}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
   8.127  \begin{isamarkuptxt}%
   8.128  \begin{isabelle}%
   8.129 -\ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isacharhash}{\isadigit{3}}\ {\isacharslash}\ {\isacharhash}{\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharhash}{\isadigit{8}}\ {\isacharslash}\ {\isacharhash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}{\isacharparenright}%
   8.130 +\ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}{\isacharparenright}%
   8.131  \end{isabelle}%
   8.132  \end{isamarkuptxt}%
   8.133  \isacommand{apply}\ simp%
   8.134  \begin{isamarkuptxt}%
   8.135  \begin{isabelle}%
   8.136 -\ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}\ {\isacharslash}\ {\isacharhash}{\isadigit{5}}{\isacharparenright}%
   8.137 +\ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{2}}\ {\isacharslash}\ {\isadigit{5}}{\isacharparenright}%
   8.138  \end{isabelle}%
   8.139  \end{isamarkuptxt}%
   8.140  \isacommand{oops}\isanewline
   8.141  \isanewline
   8.142 -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharhash}{\isadigit{3}}{\isacharslash}{\isacharhash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharhash}{\isadigit{8}}{\isacharslash}{\isacharhash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}%
   8.143 +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}%
   8.144  \begin{isamarkuptxt}%
   8.145  \begin{isabelle}%
   8.146 -\ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{3}}\ {\isacharslash}\ {\isacharhash}{\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharhash}{\isadigit{8}}\ {\isacharslash}\ {\isacharhash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ x%
   8.147 +\ {\isadigit{1}}{\isachardot}\ {\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ x%
   8.148  \end{isabelle}%
   8.149  \end{isamarkuptxt}%
   8.150  \isacommand{apply}\ simp%
   8.151  \begin{isamarkuptxt}%
   8.152  \begin{isabelle}%
   8.153 -\ {\isadigit{1}}{\isachardot}\ {\isacharhash}{\isadigit{2}}\ {\isacharless}\ x\ {\isacharasterisk}\ {\isacharhash}{\isadigit{5}}%
   8.154 +\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharless}\ x\ {\isacharasterisk}\ {\isadigit{5}}%
   8.155  \end{isabelle}%
   8.156  \end{isamarkuptxt}%
   8.157  \isacommand{oops}\isanewline
   8.158  \isanewline
   8.159 -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharhash}{\isadigit{3}}{\isacharslash}{\isacharhash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharhash}{\isadigit{1}}{\isadigit{0}}{\isacharcircum}{\isacharhash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline
   8.160 +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcircum}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline
   8.161  \isacommand{apply}\ simp\ \isanewline
   8.162  \isacommand{oops}\isanewline
   8.163  \isanewline
     9.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex	Mon Oct 08 12:27:19 2001 +0200
     9.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex	Mon Oct 08 12:28:43 2001 +0200
     9.3 @@ -26,7 +26,7 @@
     9.4  some typical examples:
     9.5  \begin{quote}
     9.6  \isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\
     9.7 -\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}\\
     9.8 +\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}{\isasymColon}{\isacharprime}a\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}\\
     9.9  \isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}A{\isachardot}\ x{\isacharequal}y}\\
    9.10  \isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}\ x{\isacharequal}z{\isacharbraceright}}\\
    9.11  \isa{{\isasymUnion}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A{\isachardot}\ {\isacharbraceleft}x\ {\isacharplus}\ y{\isacharbraceright}}
    10.1 --- a/doc-src/TutorialI/isabellesym.sty	Mon Oct 08 12:27:19 2001 +0200
    10.2 +++ b/doc-src/TutorialI/isabellesym.sty	Mon Oct 08 12:28:43 2001 +0200
    10.3 @@ -209,6 +209,8 @@
    10.4  \newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires latexsym
    10.5  \newcommand{\isasymturnstile}{\isamath{\vdash}}
    10.6  \newcommand{\isasymTurnstile}{\isamath{\models}}
    10.7 +\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\vdash}}
    10.8 +\newcommand{\isasymtturnstile}{\isamath{\mid\models}}
    10.9  \newcommand{\isasymstileturn}{\isamath{\dashv}}
   10.10  \newcommand{\isasymsurd}{\isamath{\surd}}
   10.11  \newcommand{\isasymle}{\isamath{\le}}
   10.12 @@ -337,4 +339,3 @@
   10.13  \newcommand{\isasymdieresis}{\isatext{\"\relax}}
   10.14  \newcommand{\isasymcedilla}{\isatext{\c\relax}}
   10.15  \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
   10.16 -