1.1 --- a/doc-src/TutorialI/CTL/document/Base.tex Wed Jan 29 11:02:08 2003 +0100
1.2 +++ b/doc-src/TutorialI/CTL/document/Base.tex Wed Jan 29 16:29:38 2003 +0100
1.3 @@ -98,7 +98,6 @@
1.4 telling us which atomic propositions are true in each state.%
1.5 \end{isamarkuptext}%
1.6 \isamarkuptrue%
1.7 -\isanewline
1.8 \isamarkupfalse%
1.9 \end{isabellebody}%
1.10 %%% Local Variables:
2.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex Wed Jan 29 11:02:08 2003 +0100
2.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Jan 29 16:29:38 2003 +0100
2.3 @@ -16,7 +16,6 @@
2.4 \isa{formula} by a new constructor%
2.5 \end{isamarkuptext}%
2.6 \isamarkuptrue%
2.7 -\isanewline
2.8 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula\isamarkupfalse%
2.9 %
2.10 \begin{isamarkuptext}%
2.11 @@ -40,7 +39,6 @@
2.12 \end{isamarkuptext}%
2.13 \isamarkuptrue%
2.14 \isamarkupfalse%
2.15 -\isanewline
2.16 {\isachardoublequote}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
2.17 %
2.18 \begin{isamarkuptext}%
2.19 @@ -59,7 +57,6 @@
2.20 \end{isamarkuptext}%
2.21 \isamarkuptrue%
2.22 \isamarkupfalse%
2.23 -\isanewline
2.24 {\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
2.25 %
2.26 \begin{isamarkuptext}%
2.27 @@ -483,7 +480,6 @@
2.28 \index{CTL|)}%
2.29 \end{isamarkuptext}%
2.30 \isamarkuptrue%
2.31 -\isanewline
2.32 \isamarkupfalse%
2.33 \end{isabellebody}%
2.34 %%% Local Variables:
3.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jan 29 11:02:08 2003 +0100
3.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jan 29 16:29:38 2003 +0100
3.3 @@ -181,7 +181,6 @@
3.4 \isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
3.5 \isanewline
3.6 \isamarkupfalse%
3.7 -\isanewline
3.8 \isamarkupfalse%
3.9 \end{isabellebody}%
3.10 %%% Local Variables:
4.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex Wed Jan 29 11:02:08 2003 +0100
4.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Wed Jan 29 16:29:38 2003 +0100
4.3 @@ -253,7 +253,6 @@
4.4 \isamarkupfalse%
4.5 \isamarkupfalse%
4.6 \isamarkupfalse%
4.7 -\isanewline
4.8 \isamarkupfalse%
4.9 \end{isabellebody}%
4.10 %%% Local Variables:
5.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Jan 29 11:02:08 2003 +0100
5.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Jan 29 16:29:38 2003 +0100
5.3 @@ -96,8 +96,7 @@
5.4 execution of a compiled expression results in the value of the expression:%
5.5 \end{isamarkuptext}%
5.6 \isamarkuptrue%
5.7 -\isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}\isanewline
5.8 -\isamarkupfalse%
5.9 +\isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}\isamarkupfalse%
5.10 \isamarkupfalse%
5.11 %
5.12 \begin{isamarkuptext}%
5.13 @@ -126,8 +125,7 @@
5.14 automatic case splitting, which finishes the proof:%
5.15 \end{isamarkuptxt}%
5.16 \isamarkuptrue%
5.17 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isanewline
5.18 -\isamarkupfalse%
5.19 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
5.20 \isamarkupfalse%
5.21 %
5.22 \begin{isamarkuptext}%
5.23 @@ -139,8 +137,7 @@
5.24 \isamarkuptrue%
5.25 \isamarkupfalse%
5.26 \isamarkupfalse%
5.27 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isanewline
5.28 -\isamarkupfalse%
5.29 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
5.30 \isamarkupfalse%
5.31 %
5.32 \begin{isamarkuptext}%
6.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed Jan 29 11:02:08 2003 +0100
6.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed Jan 29 16:29:38 2003 +0100
6.3 @@ -110,8 +110,7 @@
6.4 The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
6.5 \end{isamarkuptxt}%
6.6 \isamarkuptrue%
6.7 -\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
6.8 -\isamarkupfalse%
6.9 +\isacommand{apply}\ simp{\isacharunderscore}all\isamarkupfalse%
6.10 \isamarkupfalse%
6.11 %
6.12 \begin{isamarkuptext}%
7.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Wed Jan 29 11:02:08 2003 +0100
7.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Wed Jan 29 16:29:38 2003 +0100
7.3 @@ -45,8 +45,7 @@
7.4 \isamarkupfalse%
7.5 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
7.6 \isamarkupfalse%
7.7 -\isacommand{done}\isanewline
7.8 -\isamarkupfalse%
7.9 +\isacommand{done}\isamarkupfalse%
7.10 \isamarkupfalse%
7.11 \isamarkupfalse%
7.12 %
8.1 --- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Wed Jan 29 11:02:08 2003 +0100
8.2 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Wed Jan 29 16:29:38 2003 +0100
8.3 @@ -3,8 +3,7 @@
8.4 \def\isabellecontext{unfoldnested}%
8.5 \isamarkupfalse%
8.6 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
8.7 -\isakeyword{and}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
8.8 -\isamarkupfalse%
8.9 +\isakeyword{and}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isamarkupfalse%
8.10 \isamarkupfalse%
8.11 \end{isabellebody}%
8.12 %%% Local Variables:
9.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex Wed Jan 29 11:02:08 2003 +0100
9.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Wed Jan 29 16:29:38 2003 +0100
9.3 @@ -129,8 +129,7 @@
9.4 \isamarkupfalse%
9.5 \isacommand{constdefs}\isanewline
9.6 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
9.7 -\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
9.8 -\isamarkupfalse%
9.9 +\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
9.10 \isamarkupfalse%
9.11 %
9.12 \begin{isamarkuptext}%
9.13 @@ -154,8 +153,7 @@
9.14 \isanewline
9.15 \isamarkupfalse%
9.16 \isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
9.17 -\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
9.18 -\isamarkupfalse%
9.19 +\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
9.20 \isamarkupfalse%
9.21 %
9.22 \begin{isamarkuptext}%
10.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed Jan 29 11:02:08 2003 +0100
10.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed Jan 29 16:29:38 2003 +0100
10.3 @@ -157,8 +157,7 @@
10.4 \end{isamarkuptext}%
10.5 \isamarkuptrue%
10.6 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
10.7 -\ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}\isanewline
10.8 -\isamarkupfalse%
10.9 +\ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}\isamarkupfalse%
10.10 \isamarkupfalse%
10.11 \isamarkupfalse%
10.12 \isamarkupfalse%
10.13 @@ -188,8 +187,7 @@
10.14 normality of \isa{normif}:%
10.15 \end{isamarkuptext}%
10.16 \isamarkuptrue%
10.17 -\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isanewline
10.18 -\isamarkupfalse%
10.19 +\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
10.20 \isamarkupfalse%
10.21 \isamarkupfalse%
10.22 \isamarkupfalse%
11.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex Wed Jan 29 11:02:08 2003 +0100
11.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed Jan 29 16:29:38 2003 +0100
11.3 @@ -224,8 +224,7 @@
11.4 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
11.5 \end{isamarkuptxt}%
11.6 \isamarkuptrue%
11.7 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isanewline
11.8 -\isamarkupfalse%
11.9 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
11.10 \isamarkupfalse%
11.11 %
11.12 \begin{isamarkuptxt}%
11.13 @@ -241,8 +240,7 @@
11.14 \isamarkuptrue%
11.15 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
11.16 \ \isamarkupfalse%
11.17 -\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isanewline
11.18 -\isamarkupfalse%
11.19 +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
11.20 \isamarkupfalse%
11.21 %
11.22 \begin{isamarkuptxt}%
12.1 --- a/doc-src/TutorialI/Inductive/document/Mutual.tex Wed Jan 29 11:02:08 2003 +0100
12.2 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Wed Jan 29 16:29:38 2003 +0100
12.3 @@ -67,7 +67,6 @@
12.4 \isamarkupfalse%
12.5 \isamarkupfalse%
12.6 \isamarkupfalse%
12.7 -\isanewline
12.8 \isamarkupfalse%
12.9 \isamarkupfalse%
12.10 \end{isabellebody}%
13.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Jan 29 11:02:08 2003 +0100
13.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Jan 29 16:29:38 2003 +0100
13.3 @@ -64,8 +64,7 @@
13.4 \end{isamarkuptxt}%
13.5 \isamarkuptrue%
13.6 \isamarkupfalse%
13.7 -\isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline
13.8 -\isamarkupfalse%
13.9 +\isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isamarkupfalse%
13.10 \isamarkupfalse%
13.11 %
13.12 \begin{isamarkuptxt}%
13.13 @@ -247,8 +246,7 @@
13.14 We could have included this derivation in the original statement of the lemma:%
13.15 \end{isamarkuptext}%
13.16 \isamarkuptrue%
13.17 -\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isanewline
13.18 -\isamarkupfalse%
13.19 +\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isamarkupfalse%
13.20 \isamarkupfalse%
13.21 %
13.22 \begin{isamarkuptext}%
14.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex Wed Jan 29 11:02:08 2003 +0100
14.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Jan 29 16:29:38 2003 +0100
14.3 @@ -92,8 +92,7 @@
14.4 \end{isamarkuptxt}%
14.5 \isamarkuptrue%
14.6 \isamarkupfalse%
14.7 -\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isanewline
14.8 -\isamarkupfalse%
14.9 +\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse%
14.10 \isamarkupfalse%
14.11 %
14.12 \begin{isamarkuptxt}%
14.13 @@ -120,8 +119,7 @@
14.14 \end{isamarkuptxt}%
14.15 \isamarkuptrue%
14.16 \isamarkupfalse%
14.17 -\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isanewline
14.18 -\isamarkupfalse%
14.19 +\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse%
14.20 \isamarkupfalse%
14.21 %
14.22 \begin{isamarkuptext}%
15.1 --- a/doc-src/TutorialI/Misc/document/Plus.tex Wed Jan 29 11:02:08 2003 +0100
15.2 +++ b/doc-src/TutorialI/Misc/document/Plus.tex Wed Jan 29 16:29:38 2003 +0100
15.3 @@ -20,8 +20,7 @@
15.4 \isamarkupfalse%
15.5 \isamarkupfalse%
15.6 \isamarkupfalse%
15.7 -\isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isanewline
15.8 -\isamarkupfalse%
15.9 +\isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isamarkupfalse%
15.10 \isamarkupfalse%
15.11 \isamarkupfalse%
15.12 \end{isabellebody}%
16.1 --- a/doc-src/TutorialI/Misc/document/Tree.tex Wed Jan 29 11:02:08 2003 +0100
16.2 +++ b/doc-src/TutorialI/Misc/document/Tree.tex Wed Jan 29 16:29:38 2003 +0100
16.3 @@ -18,8 +18,7 @@
16.4 by swapping subtrees recursively. Prove%
16.5 \end{isamarkuptext}%
16.6 \isamarkuptrue%
16.7 -\isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
16.8 -\isamarkupfalse%
16.9 +\isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isamarkupfalse%
16.10 \isamarkupfalse%
16.11 \isamarkupfalse%
16.12 \isamarkupfalse%
16.13 @@ -31,8 +30,7 @@
16.14 by traversing it in infix order. Prove%
16.15 \end{isamarkuptext}%
16.16 \isamarkuptrue%
16.17 -\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\isanewline
16.18 -\isamarkupfalse%
16.19 +\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
16.20 \isamarkupfalse%
16.21 \isamarkupfalse%
16.22 \isamarkupfalse%
17.1 --- a/doc-src/TutorialI/Misc/document/Tree2.tex Wed Jan 29 11:02:08 2003 +0100
17.2 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Wed Jan 29 16:29:38 2003 +0100
17.3 @@ -11,8 +11,7 @@
17.4 argument, the accumulator:%
17.5 \end{isamarkuptext}%
17.6 \isamarkuptrue%
17.7 -\isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
17.8 -\isamarkupfalse%
17.9 +\isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
17.10 \isamarkupfalse%
17.11 %
17.12 \begin{isamarkuptext}%
17.13 @@ -22,8 +21,7 @@
17.14 \isamarkupfalse%
17.15 \isamarkupfalse%
17.16 \isamarkupfalse%
17.17 -\isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isanewline
17.18 -\isamarkupfalse%
17.19 +\isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isamarkupfalse%
17.20 \isamarkupfalse%
17.21 \isamarkupfalse%
17.22 \end{isabellebody}%
18.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Jan 29 11:02:08 2003 +0100
18.2 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Jan 29 16:29:38 2003 +0100
18.3 @@ -80,8 +80,7 @@
18.4 which is solved automatically:%
18.5 \end{isamarkuptxt}%
18.6 \isamarkuptrue%
18.7 -\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
18.8 -\isamarkupfalse%
18.9 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
18.10 \isamarkupfalse%
18.11 %
18.12 \begin{isamarkuptext}%
19.1 --- a/doc-src/TutorialI/Misc/document/fakenat.tex Wed Jan 29 11:02:08 2003 +0100
19.2 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex Wed Jan 29 16:29:38 2003 +0100
19.3 @@ -9,8 +9,7 @@
19.4 numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this:%
19.5 \end{isamarkuptext}%
19.6 \isamarkuptrue%
19.7 -\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat\isanewline
19.8 -\isamarkupfalse%
19.9 +\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat\isamarkupfalse%
19.10 \isamarkupfalse%
19.11 \end{isabellebody}%
19.12 %%% Local Variables:
20.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Jan 29 11:02:08 2003 +0100
20.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Jan 29 16:29:38 2003 +0100
20.3 @@ -78,8 +78,7 @@
20.4 simple arithmetic goals automatically:%
20.5 \end{isamarkuptext}%
20.6 \isamarkuptrue%
20.7 -\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}\isanewline
20.8 -\isamarkupfalse%
20.9 +\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}\isamarkupfalse%
20.10 \isamarkupfalse%
20.11 %
20.12 \begin{isamarkuptext}%
20.13 @@ -89,8 +88,7 @@
20.14 In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:%
20.15 \end{isamarkuptext}%
20.16 \isamarkuptrue%
20.17 -\isacommand{lemma}\ {\isachardoublequote}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequote}\isanewline
20.18 -\isamarkupfalse%
20.19 +\isacommand{lemma}\ {\isachardoublequote}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequote}\isamarkupfalse%
20.20 \isamarkupfalse%
20.21 %
20.22 \begin{isamarkuptext}%
20.23 @@ -107,8 +105,7 @@
20.24 \isamarkuptrue%
20.25 \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
20.26 \isamarkupfalse%
20.27 -\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
20.28 -\isamarkupfalse%
20.29 +\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isamarkupfalse%
20.30 \isamarkupfalse%
20.31 %
20.32 \begin{isamarkuptext}%
20.33 @@ -116,8 +113,7 @@
20.34 succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,%
20.35 \end{isamarkuptext}%
20.36 \isamarkuptrue%
20.37 -\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isanewline
20.38 -\isamarkupfalse%
20.39 +\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isamarkupfalse%
20.40 \isamarkupfalse%
20.41 %
20.42 \begin{isamarkuptext}%
21.1 --- a/doc-src/TutorialI/Misc/document/simp.tex Wed Jan 29 11:02:08 2003 +0100
21.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Jan 29 16:29:38 2003 +0100
21.3 @@ -218,8 +218,7 @@
21.4 \isamarkuptrue%
21.5 \isamarkupfalse%
21.6 \isamarkupfalse%
21.7 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isanewline
21.8 -\isamarkupfalse%
21.9 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
21.10 \isamarkupfalse%
21.11 %
21.12 \begin{isamarkuptext}%
21.13 @@ -293,8 +292,7 @@
21.14 the lemma below is proved by plain simplification:%
21.15 \end{isamarkuptext}%
21.16 \isamarkuptrue%
21.17 -\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isanewline
21.18 -\isamarkupfalse%
21.19 +\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isamarkupfalse%
21.20 \isamarkupfalse%
21.21 %
21.22 \begin{isamarkuptext}%
21.23 @@ -363,8 +361,7 @@
21.24 \isamarkuptrue%
21.25 \isamarkupfalse%
21.26 \isamarkupfalse%
21.27 -\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isanewline
21.28 -\isamarkupfalse%
21.29 +\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isamarkupfalse%
21.30 \isamarkupfalse%
21.31 %
21.32 \begin{isamarkuptext}%
21.33 @@ -385,8 +382,7 @@
21.34 \end{isamarkuptext}%
21.35 \isamarkuptrue%
21.36 \isamarkupfalse%
21.37 -\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isanewline
21.38 -\isamarkupfalse%
21.39 +\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse%
21.40 \isamarkupfalse%
21.41 %
21.42 \begin{isamarkuptext}%
21.43 @@ -454,8 +450,7 @@
21.44 \isamarkupfalse%
21.45 \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
21.46 \isamarkupfalse%
21.47 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
21.48 -\isamarkupfalse%
21.49 +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
21.50 \isamarkupfalse%
21.51 %
21.52 \begin{isamarkuptext}%
21.53 @@ -493,7 +488,6 @@
21.54 \end{isamarkuptext}%
21.55 \isamarkuptrue%
21.56 \isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
21.57 -\isanewline
21.58 \isamarkupfalse%
21.59 \isamarkupfalse%
21.60 \end{isabellebody}%
22.1 --- a/doc-src/TutorialI/Recdef/document/Nested0.tex Wed Jan 29 11:02:08 2003 +0100
22.2 +++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Wed Jan 29 16:29:38 2003 +0100
22.3 @@ -22,8 +22,7 @@
22.4 choose exercise~\ref{ex:trev-trev}:%
22.5 \end{isamarkuptext}%
22.6 \isamarkuptrue%
22.7 -\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\isanewline
22.8 -\isamarkupfalse%
22.9 +\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\isamarkupfalse%
22.10 \isamarkupfalse%
22.11 \end{isabellebody}%
22.12 %%% Local Variables:
23.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Wed Jan 29 11:02:08 2003 +0100
23.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Wed Jan 29 16:29:38 2003 +0100
23.3 @@ -5,8 +5,7 @@
23.4 \isamarkupfalse%
23.5 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline
23.6 \isamarkupfalse%
23.7 -\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isanewline
23.8 -\isamarkupfalse%
23.9 +\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse%
23.10 \isamarkupfalse%
23.11 %
23.12 \begin{isamarkuptext}%
24.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex Wed Jan 29 11:02:08 2003 +0100
24.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Wed Jan 29 16:29:38 2003 +0100
24.3 @@ -100,7 +100,6 @@
24.4 \isacommand{recdef}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline
24.5 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline
24.6 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}\isanewline
24.7 -\isanewline
24.8 \isamarkupfalse%
24.9 \isamarkupfalse%
24.10 \end{isabellebody}%
25.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex Wed Jan 29 11:02:08 2003 +0100
25.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Wed Jan 29 16:29:38 2003 +0100
25.3 @@ -112,7 +112,6 @@
25.4 \end{isamarkuptext}%
25.5 \isamarkuptrue%
25.6 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
25.7 -\isanewline
25.8 \isamarkupfalse%
25.9 \isamarkupfalse%
25.10 \end{isabellebody}%
26.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex Wed Jan 29 11:02:08 2003 +0100
26.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Wed Jan 29 16:29:38 2003 +0100
26.3 @@ -53,8 +53,7 @@
26.4 \isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
26.5 \ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
26.6 \ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isanewline
26.7 -{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isanewline
26.8 -\isamarkupfalse%
26.9 +{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isamarkupfalse%
26.10 \isamarkupfalse%
26.11 %
26.12 \begin{isamarkuptext}%
27.1 --- a/doc-src/TutorialI/Rules/rules.tex Wed Jan 29 11:02:08 2003 +0100
27.2 +++ b/doc-src/TutorialI/Rules/rules.tex Wed Jan 29 16:29:38 2003 +0100
27.3 @@ -758,7 +758,7 @@
27.4 resulting subgoal is trivial by assumption, so the \isacommand{by} command
27.5 proves it implicitly.
27.6
27.7 -We are using the \isa{erule} method it in a novel way. Hitherto,
27.8 +We are using the \isa{erule} method in a novel way. Hitherto,
27.9 the conclusion of the rule was just a variable such as~\isa{?R}, but it may
27.10 be any term. The conclusion is unified with the subgoal just as
27.11 it would be with the \isa{rule} method. At the same time \isa{erule} looks
27.12 @@ -1425,7 +1425,7 @@
27.13 \[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
27.14 This rule is seldom used for that purpose --- it can cause exponential
27.15 blow-up --- but it is occasionally used as an introduction rule
27.16 -for~$\varepsilon$-operator. Its name in HOL is \tdxbold{someI_ex}.%%
27.17 +for the~$\varepsilon$-operator. Its name in HOL is \tdxbold{someI_ex}.%%
27.18 \index{description operators|)}
27.19
27.20
28.1 --- a/doc-src/TutorialI/Types/document/Overloading.tex Wed Jan 29 11:02:08 2003 +0100
28.2 +++ b/doc-src/TutorialI/Types/document/Overloading.tex Wed Jan 29 16:29:38 2003 +0100
28.3 @@ -20,8 +20,7 @@
28.4 prefix{\isacharunderscore}def{\isacharcolon}\isanewline
28.5 \ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
28.6 strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
28.7 -\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}\isanewline
28.8 -\isamarkupfalse%
28.9 +\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}\isamarkupfalse%
28.10 \isamarkupfalse%
28.11 \end{isabellebody}%
28.12 %%% Local Variables:
29.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex Wed Jan 29 11:02:08 2003 +0100
29.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Wed Jan 29 16:29:38 2003 +0100
29.3 @@ -218,8 +218,7 @@
29.4 \end{isamarkuptext}%
29.5 \isamarkuptrue%
29.6 \isamarkupfalse%
29.7 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isanewline
29.8 -\isamarkupfalse%
29.9 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
29.10 \isamarkupfalse%
29.11 %
29.12 \begin{isamarkuptext}%
30.1 --- a/doc-src/TutorialI/tutorial.ind Wed Jan 29 11:02:08 2003 +0100
30.2 +++ b/doc-src/TutorialI/tutorial.ind Wed Jan 29 16:29:38 2003 +0100
30.3 @@ -27,10 +27,11 @@
30.4 \item \texttt {\%}, \bold{209}
30.5 \item \texttt {;}, \bold{7}
30.6 \item \isa {()} (constant), 24
30.7 + \item * trace_unify_fail (flag), 76
30.8 \item \isa {+} (tactical), 99
30.9 \item \isa {<*lex*>}, \see{lexicographic product}{1}
30.10 - \item \isa {?} (tactical), 99
30.11 - \item \texttt{|} (tactical), 99
30.12 + \item \isa {?} (tactical), 100
30.13 + \item \texttt{|} (tactical), 100
30.14
30.15 \indexspace
30.16
30.17 @@ -66,16 +67,16 @@
30.18 \item \isa {assumption} (method), 69
30.19 \item assumptions
30.20 \subitem of subgoal, 12
30.21 - \subitem renaming, 82--83
30.22 - \subitem reusing, 83
30.23 + \subitem renaming, 83
30.24 + \subitem reusing, 83--84
30.25 \item \isa {auto} (method), 38, 92
30.26 - \item \isa {axclass}, 164--170
30.27 - \item axiom of choice, 86
30.28 - \item axiomatic type classes, 164--170
30.29 + \item \isa {axclass}, 164--171
30.30 + \item axiom of choice, 87
30.31 + \item axiomatic type classes, 164--171
30.32
30.33 \indexspace
30.34
30.35 - \item \isacommand {back} (command), 78
30.36 + \item \isacommand {back} (command), 79
30.37 \item \isa {Ball} (constant), 109
30.38 \item \isa {ballI} (theorem), \bold{108}
30.39 \item \isa {best} (method), 92
30.40 @@ -87,7 +88,7 @@
30.41 \item binary trees, 18
30.42 \item binomial coefficients, 109
30.43 \item bisimulations, 116
30.44 - \item \isa {blast} (method), 89--90, 92
30.45 + \item \isa {blast} (method), 89--92
30.46 \item \isa {bool} (type), 4, 5
30.47 \item boolean expressions example, 20--22
30.48 \item \isa {bspec} (theorem), \bold{108}
30.49 @@ -103,7 +104,7 @@
30.50 \item \isa {case} expressions, 5, 6, 18
30.51 \item case distinctions, 19
30.52 \item case splits, \bold{31}
30.53 - \item \isa {case_tac} (method), 19, 101, 157
30.54 + \item \isa {case_tac} (method), 19, 102, 158
30.55 \item \isa {cases} (method), 162
30.56 \item \isacommand {chapter} (command), 59
30.57 \item \isa {clarify} (method), 91, 92
30.58 @@ -142,7 +143,7 @@
30.59 \subitem and nested recursion, 40, 44
30.60 \subitem mutually recursive, 38
30.61 \subitem nested, 180
30.62 - \item \isacommand {defer} (command), 16, 100
30.63 + \item \isacommand {defer} (command), 16, 101
30.64 \item Definitional Approach, 26
30.65 \item definitions, \bold{25}
30.66 \subitem unfolding, \bold{30}
30.67 @@ -152,7 +153,7 @@
30.68 \item descriptions
30.69 \subitem definite, 85
30.70 \subitem indefinite, 86
30.71 - \item \isa {dest} (attribute), 102
30.72 + \item \isa {dest} (attribute), 103
30.73 \item destruction rules, 71
30.74 \item \isa {diff_mult_distrib} (theorem), \bold{151}
30.75 \item difference
30.76 @@ -160,7 +161,7 @@
30.77 \item \isa {disjCI} (theorem), \bold{74}
30.78 \item \isa {disjE} (theorem), \bold{70}
30.79 \item \isa {div} (symbol), 23
30.80 - \item divides relation, 84, 95, 101--104, 152
30.81 + \item divides relation, 84, 95, 102--104, 152
30.82 \item division
30.83 \subitem by negative numbers, 153
30.84 \subitem by zero, 152
30.85 @@ -189,7 +190,7 @@
30.86 \item \isa {equalityI} (theorem), \bold{106}
30.87 \item \isa {erule} (method), 70
30.88 \item \isa {erule_tac} (method), 76
30.89 - \item Euclid's algorithm, 101--104
30.90 + \item Euclid's algorithm, 102--104
30.91 \item even numbers
30.92 \subitem defining inductively, 127--131
30.93 \item \texttt {EX}, \bold{209}
30.94 @@ -213,14 +214,14 @@
30.95 \item \isa {finite} (symbol), 109
30.96 \item \isa {Finites} (constant), 109
30.97 \item fixed points, 116
30.98 - \item flags, 5, 6, 33
30.99 + \item flags, 5, 6, 33, 76
30.100 \subitem setting and resetting, 5
30.101 \item \isa {force} (method), 91, 92
30.102 \item formal comments, \bold{61}
30.103 \item formal proof documents, \bold{57}
30.104 \item formulae, 5--6
30.105 - \item forward proof, 92--98
30.106 - \item \isa {frule} (method), 83
30.107 + \item forward proof, 93--99
30.108 + \item \isa {frule} (method), 83--84
30.109 \item \isa {frule_tac} (method), 76
30.110 \item \isa {fst} (constant), 24
30.111 \item function types, 5
30.112 @@ -231,9 +232,9 @@
30.113
30.114 \indexspace
30.115
30.116 - \item \isa {gcd} (constant), 93--94, 101--104
30.117 + \item \isa {gcd} (constant), 93--95, 102--104
30.118 \item generalizing for induction, 129
30.119 - \item generalizing induction formulae, 35
30.120 + \item generalizing induction formulae, 34
30.121 \item Girard, Jean-Yves, \fnote{71}
30.122 \item Gordon, Mike, 3
30.123 \item grammars
30.124 @@ -260,9 +261,9 @@
30.125 \item identity relation, \bold{112}
30.126 \item \isa {if} expressions, 5, 6
30.127 \subitem simplification of, 33
30.128 - \subitem splitting of, 31, 50
30.129 + \subitem splitting of, 31, 49
30.130 \item if-and-only-if, 6
30.131 - \item \isa {iff} (attribute), 90, 102, 130
30.132 + \item \isa {iff} (attribute), 90, 91, 103, 130
30.133 \item \isa {iffD1} (theorem), \bold{94}
30.134 \item \isa {iffD2} (theorem), \bold{94}
30.135 \item ignored material, \bold{64}
30.136 @@ -282,7 +283,7 @@
30.137 \subitem recursion, 51--52
30.138 \subitem structural, 19
30.139 \subitem well-founded, 115
30.140 - \item induction heuristics, 34--36
30.141 + \item induction heuristics, 33--35
30.142 \item \isacommand {inductive} (command), 127
30.143 \item inductive definition
30.144 \subitem simultaneous, 141
30.145 @@ -294,7 +295,7 @@
30.146 \item \isa {inj_on_def} (theorem), \bold{110}
30.147 \item injections, 110
30.148 \item \isa {insert} (constant), 107
30.149 - \item \isa {insert} (method), 97--98
30.150 + \item \isa {insert} (method), 97--99
30.151 \item instance, \bold{166}
30.152 \item \texttt {INT}, \bold{209}
30.153 \item \texttt {Int}, \bold{209}
30.154 @@ -330,12 +331,12 @@
30.155 \indexspace
30.156
30.157 \item $\lambda$ expressions, 5
30.158 - \item LCF, 44
30.159 - \item \isa {LEAST} (symbol), 23, 85
30.160 - \item least number operator, \see{\protect\isa{LEAST}}{85}
30.161 + \item LCF, 43
30.162 + \item \isa {LEAST} (symbol), 23, 86
30.163 + \item least number operator, \see{\protect\isa{LEAST}}{86}
30.164 \item Leibniz, Gottfried Wilhelm, 53
30.165 \item \isacommand {lemma} (command), 13
30.166 - \item \isacommand {lemmas} (command), 93, 102
30.167 + \item \isacommand {lemmas} (command), 93, 103
30.168 \item \isa {length} (symbol), 18
30.169 \item \isa {length_induct}, \bold{190}
30.170 \item \isa {less_than} (constant), 114
30.171 @@ -376,10 +377,10 @@
30.172 \item \isa {mono_def} (theorem), \bold{116}
30.173 \item monotone functions, \bold{116}, 139
30.174 \subitem and inductive definitions, 137--138
30.175 - \item \isa {more} (constant), 158, 160
30.176 + \item \isa {more} (constant), 159, 160
30.177 \item \isa {mp} (theorem), \bold{72}
30.178 \item \isa {mult_ac} (theorems), 152
30.179 - \item multiple inheritance, \bold{169}
30.180 + \item multiple inheritance, \bold{170}
30.181 \item multiset ordering, \bold{115}
30.182
30.183 \indexspace
30.184 @@ -423,12 +424,12 @@
30.185 \item pairs and tuples, 24, 155--158
30.186 \item parent theories, \bold{4}
30.187 \item pattern matching
30.188 - \subitem and \isacommand{recdef}, 48
30.189 + \subitem and \isacommand{recdef}, 47
30.190 \item patterns
30.191 \subitem higher-order, \bold{177}
30.192 \item PDL, 118--120
30.193 \item \isacommand {pr} (command), 16, 100
30.194 - \item \isacommand {prefer} (command), 16, 100
30.195 + \item \isacommand {prefer} (command), 16, 101
30.196 \item prefix annotation, 55
30.197 \item primitive recursion, \see{recursion, primitive}{1}
30.198 \item \isacommand {primrec} (command), 10, 18, 38--44
30.199 @@ -438,7 +439,7 @@
30.200 \item proof state, 12
30.201 \item proofs
30.202 \subitem abandoning, \bold{13}
30.203 - \subitem examples of failing, 87--89
30.204 + \subitem examples of failing, 88--89
30.205 \item protocols
30.206 \subitem security, 195--205
30.207
30.208 @@ -446,10 +447,10 @@
30.209
30.210 \item quantifiers, 6
30.211 \subitem and inductive definitions, 135--137
30.212 - \subitem existential, 82
30.213 + \subitem existential, 82--83
30.214 \subitem for sets, 108
30.215 \subitem instantiating, 84
30.216 - \subitem universal, 79--82
30.217 + \subitem universal, 80--82
30.218
30.219 \indexspace
30.220
30.221 @@ -483,12 +484,11 @@
30.222 \item \isa {rel_comp_def} (theorem), \bold{112}
30.223 \item relations, 111--114
30.224 \subitem well-founded, 114--115
30.225 - \item \isa {rename_tac} (method), 82--83
30.226 + \item \isa {rename_tac} (method), 83
30.227 \item \isa {rev} (constant), 10--14, 34
30.228 \item rewrite rules, \bold{27}
30.229 \subitem permutative, \bold{176}
30.230 \item rewriting, \bold{27}
30.231 - \item \isa {rotate_tac} (method), 30
30.232 \item \isa {rtrancl_refl} (theorem), \bold{112}
30.233 \item \isa {rtrancl_trans} (theorem), \bold{112}
30.234 \item rule induction, 128--130
30.235 @@ -526,19 +526,19 @@
30.236 \item simplification rule, 177--178
30.237 \item simplification rules, 28
30.238 \subitem adding and deleting, 29
30.239 - \item \isa {simplified} (attribute), 93, 96
30.240 + \item \isa {simplified} (attribute), 94, 96
30.241 \item \isa {size} (constant), 17
30.242 \item \isa {snd} (constant), 24
30.243 \item \isa {SOME} (symbol), 86
30.244 \item \texttt {SOME}, \bold{209}
30.245 \item \isa {Some} (constant), \bold{24}
30.246 - \item \isa {some_equality} (theorem), \bold{86}
30.247 - \item \isa {someI} (theorem), \bold{86}
30.248 - \item \isa {someI2} (theorem), \bold{86}
30.249 + \item \isa {some_equality} (theorem), \bold{87}
30.250 + \item \isa {someI} (theorem), \bold{87}
30.251 + \item \isa {someI2} (theorem), \bold{87}
30.252 \item \isa {someI_ex} (theorem), \bold{87}
30.253 \item sorts, 170
30.254 \item source comments, \bold{60}
30.255 - \item \isa {spec} (theorem), \bold{80}
30.256 + \item \isa {spec} (theorem), \bold{81}
30.257 \item \isa {split} (attribute), 32
30.258 \item \isa {split} (constant), 156
30.259 \item \isa {split} (method), 31, 156
30.260 @@ -548,9 +548,9 @@
30.261 \item \isa {split_if_asm} (theorem), 32
30.262 \item \isa {ssubst} (theorem), \bold{77}
30.263 \item structural induction, \see{induction, structural}{1}
30.264 - \item subclasses, 164, 169
30.265 + \item subclasses, 165, 169
30.266 \item subgoal numbering, 46
30.267 - \item \isa {subgoal_tac} (method), 98
30.268 + \item \isa {subgoal_tac} (method), 98, 99
30.269 \item subgoals, 12
30.270 \item \isacommand {subsect} (command), 59
30.271 \item \isacommand {subsection} (command), 59
30.272 @@ -558,7 +558,7 @@
30.273 \item \isa {subsetD} (theorem), \bold{106}
30.274 \item \isa {subsetI} (theorem), \bold{106}
30.275 \item \isa {subst} (method), 77
30.276 - \item substitution, 77--79
30.277 + \item substitution, 77--80
30.278 \item \isacommand {subsubsect} (command), 59
30.279 \item \isacommand {subsubsection} (command), 59
30.280 \item \isa {Suc} (constant), 22
30.281 @@ -573,7 +573,7 @@
30.282
30.283 \indexspace
30.284
30.285 - \item tacticals, 99
30.286 + \item tacticals, 99--100
30.287 \item tactics, 12
30.288 \item \isacommand {term} (command), 16
30.289 \item term rewriting, \bold{27}
30.290 @@ -582,8 +582,8 @@
30.291 \item text, \bold{61}
30.292 \item text blocks, \bold{61}
30.293 \item \isa {THE} (symbol), 85
30.294 - \item \isa {the_equality} (theorem), \bold{85}
30.295 - \item \isa {THEN} (attribute), \bold{94}, 96, 102
30.296 + \item \isa {the_equality} (theorem), \bold{86}
30.297 + \item \isa {THEN} (attribute), \bold{94}, 96, 103
30.298 \item \isacommand {theorem} (command), \bold{11}, 13
30.299 \item theories, 4
30.300 \subitem abandoning, \bold{16}
30.301 @@ -597,7 +597,7 @@
30.302 \item \isa {trancl_trans} (theorem), \bold{113}
30.303 \item transition systems, 117
30.304 \item \isacommand {translations} (command), 56
30.305 - \item tries, 44--47
30.306 + \item tries, 44--46
30.307 \item \isa {True} (constant), 5
30.308 \item \isa {truncate} (constant), 163
30.309 \item tuples, \see{pairs and tuples}{1}
30.310 @@ -609,10 +609,10 @@
30.311 \item type synonyms, 25
30.312 \item type variables, 5
30.313 \item \isacommand {typedecl} (command), 117, 171
30.314 - \item \isacommand {typedef} (command), 171--174
30.315 + \item \isacommand {typedef} (command), 172--174
30.316 \item types, 4--5
30.317 \subitem declaring, 171
30.318 - \subitem defining, 171--174
30.319 + \subitem defining, 172--174
30.320 \item \isacommand {types} (command), 25
30.321
30.322 \indexspace
30.323 @@ -625,7 +625,7 @@
30.324 \item \isa {UN_iff} (theorem), \bold{108}
30.325 \item \isa {Un_subset_iff} (theorem), \bold{106}
30.326 \item \isacommand {undo} (command), 16
30.327 - \item \isa {unfold} (method), \bold{31}
30.328 + \item \isa {unfold} (method), \bold{30}
30.329 \item unification, 76--79
30.330 \item \isa {UNION} (constant), 109
30.331 \item \texttt {Union}, \bold{209}