1.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Aug 29 15:13:10 2000 +0200
1.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Aug 29 15:43:29 2000 +0200
1.3 @@ -1,4 +1,5 @@
1.4 -\begin{isabelle}%
1.5 +%
1.6 +\begin{isabellebody}%
1.7 %
1.8 \begin{isamarkuptext}%
1.9 \noindent
1.10 @@ -111,7 +112,7 @@
1.11 However, this is unnecessary because the generalized version fully subsumes
1.12 its instance.%
1.13 \end{isamarkuptext}%
1.14 -\end{isabelle}%
1.15 +\end{isabellebody}%
1.16 %%% Local Variables:
1.17 %%% mode: latex
1.18 %%% TeX-master: "root"
2.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Tue Aug 29 15:13:10 2000 +0200
2.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Tue Aug 29 15:43:29 2000 +0200
2.3 @@ -1,4 +1,5 @@
2.4 -\begin{isabelle}%
2.5 +%
2.6 +\begin{isabellebody}%
2.7 %
2.8 \begin{isamarkuptext}%
2.9 Sometimes it is necessary to define two datatypes that depend on each
2.10 @@ -111,7 +112,7 @@
2.11 it. ({\em Hint:} proceed as in \S\ref{sec:boolex}).
2.12 \end{exercise}%
2.13 \end{isamarkuptext}%
2.14 -\end{isabelle}%
2.15 +\end{isabellebody}%
2.16 %%% Local Variables:
2.17 %%% mode: latex
2.18 %%% TeX-master: "root"
3.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Aug 29 15:13:10 2000 +0200
3.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Aug 29 15:43:29 2000 +0200
3.3 @@ -1,4 +1,5 @@
3.4 -\begin{isabelle}%
3.5 +%
3.6 +\begin{isabellebody}%
3.7 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
3.8 \begin{isamarkuptext}%
3.9 \noindent Parameter \isa{'a} is the type of values stored in
3.10 @@ -49,7 +50,7 @@
3.11 ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
3.12 \end{isabellepar}%%
3.13 \end{isamarkuptext}%
3.14 -\end{isabelle}%
3.15 +\end{isabellebody}%
3.16 %%% Local Variables:
3.17 %%% mode: latex
3.18 %%% TeX-master: "root"
4.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex Tue Aug 29 15:13:10 2000 +0200
4.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Aug 29 15:43:29 2000 +0200
4.3 @@ -1,4 +1,5 @@
4.4 -\begin{isabelle}%
4.5 +%
4.6 +\begin{isabellebody}%
4.7 %
4.8 \begin{isamarkuptext}%
4.9 So far, all datatypes had the property that on the right-hand side of their
4.10 @@ -121,7 +122,7 @@
4.11 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
4.12 expressions as its argument: \isa{Sum "'a aexp list"}.%
4.13 \end{isamarkuptext}%
4.14 -\end{isabelle}%
4.15 +\end{isabellebody}%
4.16 %%% Local Variables:
4.17 %%% mode: latex
4.18 %%% TeX-master: "root"
5.1 --- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Tue Aug 29 15:13:10 2000 +0200
5.2 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Tue Aug 29 15:43:29 2000 +0200
5.3 @@ -1,6 +1,7 @@
5.4 -\begin{isabelle}%
5.5 +%
5.6 +\begin{isabellebody}%
5.7 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
5.8 -\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabelle}%
5.9 +\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabellebody}%
5.10 %%% Local Variables:
5.11 %%% mode: latex
5.12 %%% TeX-master: "root"
6.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Aug 29 15:13:10 2000 +0200
6.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Aug 29 15:43:29 2000 +0200
6.3 @@ -1,4 +1,5 @@
6.4 -\begin{isabelle}%
6.5 +%
6.6 +\begin{isabellebody}%
6.7 %
6.8 \begin{isamarkuptext}%
6.9 \subsubsection{How can we model boolean expressions?}
6.10 @@ -131,7 +132,7 @@
6.11 and prove \isa{normal(norm b)}. Of course, this requires a lemma about
6.12 normality of \isa{normif}:%
6.13 \end{isamarkuptext}%
6.14 -\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}\end{isabelle}%
6.15 +\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}\end{isabellebody}%
6.16 %%% Local Variables:
6.17 %%% mode: latex
6.18 %%% TeX-master: "root"
7.1 --- a/doc-src/TutorialI/IsaMakefile Tue Aug 29 15:13:10 2000 +0200
7.2 +++ b/doc-src/TutorialI/IsaMakefile Tue Aug 29 15:43:29 2000 +0200
7.3 @@ -97,7 +97,7 @@
7.4
7.5 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
7.6
7.7 -$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy Misc/cases.thy \
7.8 +$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
7.9 Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \
7.10 Misc/prime_def.thy Misc/case_exprs.thy \
7.11 Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
8.1 --- a/doc-src/TutorialI/Misc/ROOT.ML Tue Aug 29 15:13:10 2000 +0200
8.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML Tue Aug 29 15:43:29 2000 +0200
8.3 @@ -1,6 +1,5 @@
8.4 use_thy "Tree";
8.5 use_thy "Tree2";
8.6 -use_thy "cases";
8.7 use_thy "case_exprs";
8.8 use_thy "fakenat";
8.9 use_thy "natsum";
9.1 --- a/doc-src/TutorialI/Misc/cases.thy Tue Aug 29 15:13:10 2000 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,39 +0,0 @@
9.4 -(*<*)
9.5 -theory "cases" = Main:;
9.6 -(*>*)
9.7 -
9.8 -subsection{*Structural induction and case distinction*}
9.9 -
9.10 -text{*
9.11 -\indexbold{structural induction}
9.12 -\indexbold{induction!structural}
9.13 -\indexbold{case distinction}
9.14 -Almost all the basic laws about a datatype are applied automatically during
9.15 -simplification. Only induction is invoked by hand via \isaindex{induct_tac},
9.16 -which works for any datatype. In some cases, induction is overkill and a case
9.17 -distinction over all constructors of the datatype suffices. This is performed
9.18 -by \isaindexbold{case_tac}. A trivial example:
9.19 -*}
9.20 -
9.21 -lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs";
9.22 -apply(case_tac xs);
9.23 -
9.24 -txt{*\noindent
9.25 -results in the proof state
9.26 -\begin{isabellepar}%
9.27 -~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
9.28 -~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
9.29 -\end{isabellepar}%
9.30 -which is solved automatically:
9.31 -*}
9.32 -
9.33 -by(auto)
9.34 -
9.35 -text{*
9.36 -Note that we do not need to give a lemma a name if we do not intend to refer
9.37 -to it explicitly in the future.
9.38 -*}
9.39 -
9.40 -(*<*)
9.41 -end
9.42 -(*>*)
10.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Aug 29 15:13:10 2000 +0200
10.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Aug 29 15:43:29 2000 +0200
10.3 @@ -1,4 +1,5 @@
10.4 -\begin{isabelle}%
10.5 +%
10.6 +\begin{isabellebody}%
10.7 %
10.8 \begin{isamarkuptext}%
10.9 \noindent
10.10 @@ -271,7 +272,7 @@
10.11 For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on \isa{nat}.
10.12 For details see the library.%
10.13 \end{isamarkuptext}%
10.14 -\end{isabelle}%
10.15 +\end{isabellebody}%
10.16 %%% Local Variables:
10.17 %%% mode: latex
10.18 %%% TeX-master: "root"
11.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 29 15:13:10 2000 +0200
11.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 29 15:43:29 2000 +0200
11.3 @@ -1,4 +1,5 @@
11.4 -\begin{isabelle}%
11.5 +%
11.6 +\begin{isabellebody}%
11.7 %
11.8 \begin{isamarkuptext}%
11.9 Function \isa{rev} has quadratic worst-case running time
11.10 @@ -88,7 +89,7 @@
11.11 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
11.12 to learn about some advanced techniques for inductive proofs.%
11.13 \end{isamarkuptxt}%
11.14 -\end{isabelle}%
11.15 +\end{isabellebody}%
11.16 %%% Local Variables:
11.17 %%% mode: latex
11.18 %%% TeX-master: "root"
12.1 --- a/doc-src/TutorialI/Misc/document/Tree.tex Tue Aug 29 15:13:10 2000 +0200
12.2 +++ b/doc-src/TutorialI/Misc/document/Tree.tex Tue Aug 29 15:43:29 2000 +0200
12.3 @@ -1,4 +1,5 @@
12.4 -\begin{isabelle}%
12.5 +%
12.6 +\begin{isabellebody}%
12.7 %
12.8 \begin{isamarkuptext}%
12.9 \noindent
12.10 @@ -16,7 +17,7 @@
12.11 Define a function \isa{flatten} that flattens a tree into a list
12.12 by traversing it in infix order. Prove%
12.13 \end{isamarkuptext}%
12.14 -\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\end{isabelle}%
12.15 +\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\end{isabellebody}%
12.16 %%% Local Variables:
12.17 %%% mode: latex
12.18 %%% TeX-master: "root"
13.1 --- a/doc-src/TutorialI/Misc/document/Tree2.tex Tue Aug 29 15:13:10 2000 +0200
13.2 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Tue Aug 29 15:43:29 2000 +0200
13.3 @@ -1,4 +1,5 @@
13.4 -\begin{isabelle}%
13.5 +%
13.6 +\begin{isabellebody}%
13.7 %
13.8 \begin{isamarkuptext}%
13.9 \noindent In Exercise~\ref{ex:Tree} we defined a function
13.10 @@ -11,7 +12,7 @@
13.11 \begin{isamarkuptext}%
13.12 \noindent Define \isa{flatten2} and prove%
13.13 \end{isamarkuptext}%
13.14 -\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabelle}%
13.15 +\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}%
13.16 %%% Local Variables:
13.17 %%% mode: latex
13.18 %%% TeX-master: "root"
14.1 --- a/doc-src/TutorialI/Misc/document/arith1.tex Tue Aug 29 15:13:10 2000 +0200
14.2 +++ b/doc-src/TutorialI/Misc/document/arith1.tex Tue Aug 29 15:43:29 2000 +0200
14.3 @@ -1,6 +1,7 @@
14.4 -\begin{isabelle}%
14.5 +%
14.6 +\begin{isabellebody}%
14.7 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
14.8 -\end{isabelle}%
14.9 +\end{isabellebody}%
14.10 %%% Local Variables:
14.11 %%% mode: latex
14.12 %%% TeX-master: "root"
15.1 --- a/doc-src/TutorialI/Misc/document/arith2.tex Tue Aug 29 15:13:10 2000 +0200
15.2 +++ b/doc-src/TutorialI/Misc/document/arith2.tex Tue Aug 29 15:43:29 2000 +0200
15.3 @@ -1,7 +1,8 @@
15.4 -\begin{isabelle}%
15.5 +%
15.6 +\begin{isabellebody}%
15.7 \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
15.8 \isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
15.9 -\end{isabelle}%
15.10 +\end{isabellebody}%
15.11 %%% Local Variables:
15.12 %%% mode: latex
15.13 %%% TeX-master: "root"
16.1 --- a/doc-src/TutorialI/Misc/document/arith3.tex Tue Aug 29 15:13:10 2000 +0200
16.2 +++ b/doc-src/TutorialI/Misc/document/arith3.tex Tue Aug 29 15:43:29 2000 +0200
16.3 @@ -1,6 +1,7 @@
16.4 -\begin{isabelle}%
16.5 +%
16.6 +\begin{isabellebody}%
16.7 \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}\isadigit{0}\ {\isasymor}\ n{\isacharequal}\isadigit{1}{\isachardoublequote}\isanewline
16.8 -\end{isabelle}%
16.9 +\end{isabellebody}%
16.10 %%% Local Variables:
16.11 %%% mode: latex
16.12 %%% TeX-master: "root"
17.1 --- a/doc-src/TutorialI/Misc/document/arith4.tex Tue Aug 29 15:13:10 2000 +0200
17.2 +++ b/doc-src/TutorialI/Misc/document/arith4.tex Tue Aug 29 15:43:29 2000 +0200
17.3 @@ -1,6 +1,7 @@
17.4 -\begin{isabelle}%
17.5 +%
17.6 +\begin{isabellebody}%
17.7 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
17.8 -\end{isabelle}%
17.9 +\end{isabellebody}%
17.10 %%% Local Variables:
17.11 %%% mode: latex
17.12 %%% TeX-master: "root"
18.1 --- a/doc-src/TutorialI/Misc/document/asm_simp.tex Tue Aug 29 15:13:10 2000 +0200
18.2 +++ b/doc-src/TutorialI/Misc/document/asm_simp.tex Tue Aug 29 15:43:29 2000 +0200
18.3 @@ -1,4 +1,5 @@
18.4 -\begin{isabelle}%
18.5 +%
18.6 +\begin{isabellebody}%
18.7 %
18.8 \begin{isamarkuptext}%
18.9 By default, assumptions are part of the simplification process: they are used
18.10 @@ -44,7 +45,7 @@
18.11 Note that only one of the above options is allowed, and it must precede all
18.12 other arguments.%
18.13 \end{isamarkuptext}%
18.14 -\end{isabelle}%
18.15 +\end{isabellebody}%
18.16 %%% Local Variables:
18.17 %%% mode: latex
18.18 %%% TeX-master: "root"
19.1 --- a/doc-src/TutorialI/Misc/document/case_splits.tex Tue Aug 29 15:13:10 2000 +0200
19.2 +++ b/doc-src/TutorialI/Misc/document/case_splits.tex Tue Aug 29 15:43:29 2000 +0200
19.3 @@ -1,4 +1,5 @@
19.4 -\begin{isabelle}%
19.5 +%
19.6 +\begin{isabellebody}%
19.7 %
19.8 \begin{isamarkuptext}%
19.9 Goals containing \isaindex{if}-expressions are usually proved by case
19.10 @@ -82,7 +83,7 @@
19.11 If you need to split both in the assumptions and the conclusion,
19.12 use $t$\isa{.splits} which subsumes $t$\isa{.split} and $t$\isa{.split_asm}.%
19.13 \end{isamarkuptxt}%
19.14 -\end{isabelle}%
19.15 +\end{isabellebody}%
19.16 %%% Local Variables:
19.17 %%% mode: latex
19.18 %%% TeX-master: "root"
20.1 --- a/doc-src/TutorialI/Misc/document/cases.tex Tue Aug 29 15:13:10 2000 +0200
20.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
20.3 @@ -1,35 +0,0 @@
20.4 -\begin{isabelle}%
20.5 -%
20.6 -\isamarkupsubsection{Structural induction and case distinction}
20.7 -%
20.8 -\begin{isamarkuptext}%
20.9 -\indexbold{structural induction}
20.10 -\indexbold{induction!structural}
20.11 -\indexbold{case distinction}
20.12 -Almost all the basic laws about a datatype are applied automatically during
20.13 -simplification. Only induction is invoked by hand via \isaindex{induct_tac},
20.14 -which works for any datatype. In some cases, induction is overkill and a case
20.15 -distinction over all constructors of the datatype suffices. This is performed
20.16 -by \isaindexbold{case_tac}. A trivial example:%
20.17 -\end{isamarkuptext}%
20.18 -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
20.19 -\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
20.20 -\begin{isamarkuptxt}%
20.21 -\noindent
20.22 -results in the proof state
20.23 -\begin{isabellepar}%
20.24 -~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
20.25 -~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
20.26 -\end{isabellepar}%
20.27 -which is solved automatically:%
20.28 -\end{isamarkuptxt}%
20.29 -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
20.30 -\begin{isamarkuptext}%
20.31 -Note that we do not need to give a lemma a name if we do not intend to refer
20.32 -to it explicitly in the future.%
20.33 -\end{isamarkuptext}%
20.34 -\end{isabelle}%
20.35 -%%% Local Variables:
20.36 -%%% mode: latex
20.37 -%%% TeX-master: "root"
20.38 -%%% End:
21.1 --- a/doc-src/TutorialI/Misc/document/cond_rewr.tex Tue Aug 29 15:13:10 2000 +0200
21.2 +++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex Tue Aug 29 15:43:29 2000 +0200
21.3 @@ -1,4 +1,5 @@
21.4 -\begin{isabelle}%
21.5 +%
21.6 +\begin{isabellebody}%
21.7 %
21.8 \begin{isamarkuptext}%
21.9 So far all examples of rewrite rules were equations. The simplifier also
21.10 @@ -23,7 +24,7 @@
21.11 simplifies to \isa{xs \isasymnoteq\ []}, which is exactly the local
21.12 assumption of the subgoal.%
21.13 \end{isamarkuptext}%
21.14 -\end{isabelle}%
21.15 +\end{isabellebody}%
21.16 %%% Local Variables:
21.17 %%% mode: latex
21.18 %%% TeX-master: "root"
22.1 --- a/doc-src/TutorialI/Misc/document/def_rewr.tex Tue Aug 29 15:13:10 2000 +0200
22.2 +++ b/doc-src/TutorialI/Misc/document/def_rewr.tex Tue Aug 29 15:43:29 2000 +0200
22.3 @@ -1,4 +1,5 @@
22.4 -\begin{isabelle}%
22.5 +%
22.6 +\begin{isabellebody}%
22.7 %
22.8 \begin{isamarkuptext}%
22.9 \noindent Constant definitions (\S\ref{sec:ConstDefinitions}) can
22.10 @@ -38,7 +39,7 @@
22.11 You should normally not turn a definition permanently into a simplification
22.12 rule because this defeats the whole purpose of an abbreviation.%
22.13 \end{isamarkuptext}%
22.14 -\end{isabelle}%
22.15 +\end{isabellebody}%
22.16 %%% Local Variables:
22.17 %%% mode: latex
22.18 %%% TeX-master: "root"
23.1 --- a/doc-src/TutorialI/Misc/document/fakenat.tex Tue Aug 29 15:13:10 2000 +0200
23.2 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex Tue Aug 29 15:43:29 2000 +0200
23.3 @@ -1,11 +1,12 @@
23.4 -\begin{isabelle}%
23.5 +%
23.6 +\begin{isabellebody}%
23.7 %
23.8 \begin{isamarkuptext}%
23.9 \noindent
23.10 The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural
23.11 numbers is predefined and behaves like%
23.12 \end{isamarkuptext}%
23.13 -\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabelle}%
23.14 +\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabellebody}%
23.15 %%% Local Variables:
23.16 %%% mode: latex
23.17 %%% TeX-master: "root"
24.1 --- a/doc-src/TutorialI/Misc/document/let_rewr.tex Tue Aug 29 15:13:10 2000 +0200
24.2 +++ b/doc-src/TutorialI/Misc/document/let_rewr.tex Tue Aug 29 15:43:29 2000 +0200
24.3 @@ -1,11 +1,12 @@
24.4 -\begin{isabelle}%
24.5 +%
24.6 +\begin{isabellebody}%
24.7 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
24.8 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
24.9 \begin{isamarkuptext}%
24.10 If, in a particular context, there is no danger of a combinatorial explosion
24.11 of nested \isa{let}s one could even add \isa{Let_def} permanently:%
24.12 \end{isamarkuptext}%
24.13 -\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabelle}%
24.14 +\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabellebody}%
24.15 %%% Local Variables:
24.16 %%% mode: latex
24.17 %%% TeX-master: "root"
25.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex Tue Aug 29 15:13:10 2000 +0200
25.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Tue Aug 29 15:43:29 2000 +0200
25.3 @@ -1,4 +1,5 @@
25.4 -\begin{isabelle}%
25.5 +%
25.6 +\begin{isabellebody}%
25.7 %
25.8 \begin{isamarkuptext}%
25.9 \noindent
25.10 @@ -22,7 +23,7 @@
25.11 \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
25.12 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
25.13 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
25.14 -\end{isabelle}%
25.15 +\end{isabellebody}%
25.16 %%% Local Variables:
25.17 %%% mode: latex
25.18 %%% TeX-master: "root"
26.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex Tue Aug 29 15:13:10 2000 +0200
26.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Tue Aug 29 15:43:29 2000 +0200
26.3 @@ -1,4 +1,5 @@
26.4 -\begin{isabelle}%
26.5 +%
26.6 +\begin{isabellebody}%
26.7 %
26.8 \begin{isamarkuptext}%
26.9 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
26.10 @@ -20,7 +21,7 @@
26.11 \end{quote}
26.12 Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
26.13 \end{isamarkuptext}%
26.14 -\end{isabelle}%
26.15 +\end{isabellebody}%
26.16 %%% Local Variables:
26.17 %%% mode: latex
26.18 %%% TeX-master: "root"
27.1 --- a/doc-src/TutorialI/Misc/document/prime_def.tex Tue Aug 29 15:13:10 2000 +0200
27.2 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex Tue Aug 29 15:43:29 2000 +0200
27.3 @@ -1,4 +1,5 @@
27.4 -\begin{isabelle}%
27.5 +%
27.6 +\begin{isabellebody}%
27.7 \isanewline
27.8 \ \ \ \ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
27.9 \begin{isamarkuptext}%
27.10 @@ -8,7 +9,7 @@
27.11 right-hand side, which would introduce an inconsistency (why?). What you
27.12 should have written is%
27.13 \end{isamarkuptext}%
27.14 -\ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabelle}%
27.15 +\ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabellebody}%
27.16 %%% Local Variables:
27.17 %%% mode: latex
27.18 %%% TeX-master: "root"
28.1 --- a/doc-src/TutorialI/Misc/document/trace_simp.tex Tue Aug 29 15:13:10 2000 +0200
28.2 +++ b/doc-src/TutorialI/Misc/document/trace_simp.tex Tue Aug 29 15:43:29 2000 +0200
28.3 @@ -1,4 +1,5 @@
28.4 -\begin{isabelle}%
28.5 +%
28.6 +\begin{isabellebody}%
28.7 %
28.8 \begin{isamarkuptext}%
28.9 Using the simplifier effectively may take a bit of experimentation. Set the
28.10 @@ -36,7 +37,7 @@
28.11 of rewrite rules). Thus it is advisable to reset it:%
28.12 \end{isamarkuptxt}%
28.13 \isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
28.14 -\end{isabelle}%
28.15 +\end{isabellebody}%
28.16 %%% Local Variables:
28.17 %%% mode: latex
28.18 %%% TeX-master: "root"
29.1 --- a/doc-src/TutorialI/Misc/document/types.tex Tue Aug 29 15:13:10 2000 +0200
29.2 +++ b/doc-src/TutorialI/Misc/document/types.tex Tue Aug 29 15:43:29 2000 +0200
29.3 @@ -1,4 +1,5 @@
29.4 -\begin{isabelle}%
29.5 +%
29.6 +\begin{isabellebody}%
29.7 \isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
29.8 \ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
29.9 \ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
29.10 @@ -38,7 +39,7 @@
29.11 in which case the default name of each definition is \isa{$f$_def}, where
29.12 $f$ is the name of the defined constant.%
29.13 \end{isamarkuptext}%
29.14 -\end{isabelle}%
29.15 +\end{isabellebody}%
29.16 %%% Local Variables:
29.17 %%% mode: latex
29.18 %%% TeX-master: "root"
30.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 29 15:13:10 2000 +0200
30.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 29 15:43:29 2000 +0200
30.3 @@ -1,4 +1,5 @@
30.4 -\begin{isabelle}%
30.5 +%
30.6 +\begin{isabellebody}%
30.7 %
30.8 \begin{isamarkuptext}%
30.9 Assuming we have defined our function such that Isabelle could prove
30.10 @@ -62,7 +63,7 @@
30.11 empty list, the singleton list, and the list with at least two elements
30.12 (in which case you may assume it holds for the tail of that list).%
30.13 \end{isamarkuptext}%
30.14 -\end{isabelle}%
30.15 +\end{isabellebody}%
30.16 %%% Local Variables:
30.17 %%% mode: latex
30.18 %%% TeX-master: "root"
31.1 --- a/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Aug 29 15:13:10 2000 +0200
31.2 +++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Aug 29 15:43:29 2000 +0200
31.3 @@ -1,4 +1,5 @@
31.4 -\begin{isabelle}%
31.5 +%
31.6 +\begin{isabellebody}%
31.7 %
31.8 \begin{isamarkuptext}%
31.9 In \S\ref{sec:nested-datatype} we defined the datatype of terms%
31.10 @@ -16,7 +17,7 @@
31.11
31.12 FIXME: declare trev now!%
31.13 \end{isamarkuptext}%
31.14 -\end{isabelle}%
31.15 +\end{isabellebody}%
31.16 %%% Local Variables:
31.17 %%% mode: latex
31.18 %%% TeX-master: "root"
32.1 --- a/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Aug 29 15:13:10 2000 +0200
32.2 +++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Aug 29 15:43:29 2000 +0200
32.3 @@ -1,4 +1,5 @@
32.4 -\begin{isabelle}%
32.5 +%
32.6 +\begin{isabellebody}%
32.7 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
32.8 \begin{isamarkuptext}%
32.9 \noindent
32.10 @@ -38,7 +39,7 @@
32.11 We will now prove the termination condition and continue with our definition.
32.12 Below we return to the question of how \isacommand{recdef} ``knows'' about \isa{map}.%
32.13 \end{isamarkuptext}%
32.14 -\end{isabelle}%
32.15 +\end{isabellebody}%
32.16 %%% Local Variables:
32.17 %%% mode: latex
32.18 %%% TeX-master: "root"
33.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Aug 29 15:13:10 2000 +0200
33.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Aug 29 15:43:29 2000 +0200
33.3 @@ -1,4 +1,5 @@
33.4 -\begin{isabelle}%
33.5 +%
33.6 +\begin{isabellebody}%
33.7 %
33.8 \begin{isamarkuptext}%
33.9 \noindent
33.10 @@ -90,7 +91,7 @@
33.11 declaring a congruence rule for the simplifier does not make it
33.12 available to \isacommand{recdef}, and vice versa. This is intentional.%
33.13 \end{isamarkuptext}%
33.14 -\end{isabelle}%
33.15 +\end{isabellebody}%
33.16 %%% Local Variables:
33.17 %%% mode: latex
33.18 %%% TeX-master: "root"
34.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex Tue Aug 29 15:13:10 2000 +0200
34.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Aug 29 15:43:29 2000 +0200
34.3 @@ -1,4 +1,5 @@
34.4 -\begin{isabelle}%
34.5 +%
34.6 +\begin{isabellebody}%
34.7 %
34.8 \begin{isamarkuptext}%
34.9 Here is a simple example, the Fibonacci function:%
34.10 @@ -77,7 +78,7 @@
34.11 For non-recursive functions the termination measure degenerates to the empty
34.12 set \isa{\{\}}.%
34.13 \end{isamarkuptext}%
34.14 -\end{isabelle}%
34.15 +\end{isabellebody}%
34.16 %%% Local Variables:
34.17 %%% mode: latex
34.18 %%% TeX-master: "root"
35.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex Tue Aug 29 15:13:10 2000 +0200
35.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Tue Aug 29 15:43:29 2000 +0200
35.3 @@ -1,4 +1,5 @@
35.4 -\begin{isabelle}%
35.5 +%
35.6 +\begin{isabellebody}%
35.7 %
35.8 \begin{isamarkuptext}%
35.9 Once we have succeeded in proving all termination conditions, the recursion
35.10 @@ -100,7 +101,7 @@
35.11 after which we can disable the original simplification rule:%
35.12 \end{isamarkuptext}%
35.13 \isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ gcd{\isachardot}simps\isanewline
35.14 -\end{isabelle}%
35.15 +\end{isabellebody}%
35.16 %%% Local Variables:
35.17 %%% mode: latex
35.18 %%% TeX-master: "root"
36.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex Tue Aug 29 15:13:10 2000 +0200
36.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Tue Aug 29 15:43:29 2000 +0200
36.3 @@ -1,4 +1,5 @@
36.4 -\begin{isabelle}%
36.5 +%
36.6 +\begin{isabellebody}%
36.7 %
36.8 \begin{isamarkuptext}%
36.9 When a function is defined via \isacommand{recdef}, Isabelle tries to prove
36.10 @@ -86,7 +87,7 @@
36.11 For details see the manual~\cite{isabelle-HOL} and the examples in the
36.12 library.%
36.13 \end{isamarkuptext}%
36.14 -\end{isabelle}%
36.15 +\end{isabellebody}%
36.16 %%% Local Variables:
36.17 %%% mode: latex
36.18 %%% TeX-master: "root"
37.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Aug 29 15:13:10 2000 +0200
37.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Aug 29 15:43:29 2000 +0200
37.3 @@ -1,4 +1,5 @@
37.4 -\begin{isabelle}%
37.5 +%
37.6 +\begin{isabellebody}%
37.7 \isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}%
37.8 \begin{isamarkuptext}%
37.9 \noindent
37.10 @@ -324,7 +325,7 @@
37.11 we are finished with its development:%
37.12 \end{isamarkuptext}%
37.13 \isacommand{end}\isanewline
37.14 -\end{isabelle}%
37.15 +\end{isabellebody}%
37.16 %%% Local Variables:
37.17 %%% mode: latex
37.18 %%% TeX-master: "root"
38.1 --- a/doc-src/TutorialI/Trie/document/Option2.tex Tue Aug 29 15:13:10 2000 +0200
38.2 +++ b/doc-src/TutorialI/Trie/document/Option2.tex Tue Aug 29 15:43:29 2000 +0200
38.3 @@ -1,6 +1,7 @@
38.4 -\begin{isabelle}%
38.5 +%
38.6 +\begin{isabellebody}%
38.7 \isanewline
38.8 -\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabelle}%
38.9 +\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
38.10 %%% Local Variables:
38.11 %%% mode: latex
38.12 %%% TeX-master: "root"
39.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex Tue Aug 29 15:13:10 2000 +0200
39.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Tue Aug 29 15:43:29 2000 +0200
39.3 @@ -1,4 +1,5 @@
39.4 -\begin{isabelle}%
39.5 +%
39.6 +\begin{isabellebody}%
39.7 %
39.8 \begin{isamarkuptext}%
39.9 To minimize running time, each node of a trie should contain an array that maps
39.10 @@ -122,7 +123,7 @@
39.11 solves the proof. Part~\ref{Isar} shows you how to write readable and stable
39.12 proofs.%
39.13 \end{isamarkuptext}%
39.14 -\end{isabelle}%
39.15 +\end{isabellebody}%
39.16 %%% Local Variables:
39.17 %%% mode: latex
39.18 %%% TeX-master: "root"