author | wenzelm |
Thu, 26 Jul 2012 18:55:42 +0200 | |
changeset 48522 | 708278fc2dff |
parent 48519 | 5deda0549f97 |
permissions | -rw-r--r-- |
9722 | 1 |
% |
2 |
\begin{isabellebody}% |
|
9924 | 3 |
\def\isabellecontext{Nested}% |
17056 | 4 |
% |
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
% |
|
11 |
\endisatagtheory |
|
12 |
{\isafoldtheory}% |
|
13 |
% |
|
14 |
\isadelimtheory |
|
15 |
% |
|
16 |
\endisadelimtheory |
|
8749 | 17 |
% |
18 |
\begin{isamarkuptext}% |
|
11458 | 19 |
\index{datatypes!and nested recursion}% |
8749 | 20 |
So far, all datatypes had the property that on the right-hand side of their |
11458 | 21 |
definition they occurred only at the top-level: directly below a |
11256 | 22 |
constructor. Now we consider \emph{nested recursion}, where the recursive |
11310 | 23 |
datatype occurs nested in some other datatype (but not inside itself!). |
11256 | 24 |
Consider the following model of terms |
8749 | 25 |
where function symbols can be applied to a list of arguments:% |
26 |
\end{isamarkuptext}% |
|
17175 | 27 |
\isamarkuptrue% |
28 |
\isacommand{datatype}\isamarkupfalse% |
|
40406 | 29 |
\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteopen}}term{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ {\isaliteral{27}{\isacharprime}}v\ {\isaliteral{7C}{\isacharbar}}\ App\ {\isaliteral{27}{\isacharprime}}f\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list{\isaliteral{22}{\isachardoublequoteclose}}% |
8749 | 30 |
\begin{isamarkuptext}% |
31 |
\noindent |
|
32 |
Note that we need to quote \isa{term} on the left to avoid confusion with |
|
10171 | 33 |
the Isabelle command \isacommand{term}. |
40406 | 34 |
Parameter \isa{{\isaliteral{27}{\isacharprime}}v} is the type of variables and \isa{{\isaliteral{27}{\isacharprime}}f} the type of |
8749 | 35 |
function symbols. |
40406 | 36 |
A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isaliteral{5B}{\isacharbrackleft}}Var\ x{\isaliteral{2C}{\isacharcomma}}\ App\ g\ {\isaliteral{5B}{\isacharbrackleft}}Var\ y{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are |
8749 | 37 |
suitable values, e.g.\ numbers or strings. |
38 |
||
39 |
What complicates the definition of \isa{term} is the nested occurrence of |
|
40 |
\isa{term} inside \isa{list} on the right-hand side. In principle, |
|
41 |
nested recursion can be eliminated in favour of mutual recursion by unfolding |
|
42 |
the offending datatypes, here \isa{list}. The result for \isa{term} |
|
43 |
would be something like |
|
8751 | 44 |
\medskip |
45 |
||
48522 | 46 |
\input{document/unfoldnested.tex} |
8751 | 47 |
\medskip |
48 |
||
49 |
\noindent |
|
8749 | 50 |
Although we do not recommend this unfolding to the user, it shows how to |
51 |
simulate nested recursion by mutual recursion. |
|
52 |
Now we return to the initial definition of \isa{term} using |
|
53 |
nested recursion. |
|
54 |
||
55 |
Let us define a substitution function on terms. Because terms involve term |
|
56 |
lists, we need to define two substitution functions simultaneously:% |
|
57 |
\end{isamarkuptext}% |
|
17175 | 58 |
\isamarkuptrue% |
59 |
\isacommand{primrec}\isamarkupfalse% |
|
60 |
\isanewline |
|
40406 | 61 |
subst\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ \ \ \ \ \ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline |
62 |
substs{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
27015 | 63 |
\isakeyword{where}\isanewline |
40406 | 64 |
{\isaliteral{22}{\isachardoublequoteopen}}subst\ s\ {\isaliteral{28}{\isacharparenleft}}Var\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ s\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
65 |
\ \ subst{\isaliteral{5F}{\isacharunderscore}}App{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
66 |
{\isaliteral{22}{\isachardoublequoteopen}}subst\ s\ {\isaliteral{28}{\isacharparenleft}}App\ f\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ f\ {\isaliteral{28}{\isacharparenleft}}substs\ s\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
8749 | 67 |
\isanewline |
40406 | 68 |
{\isaliteral{22}{\isachardoublequoteopen}}substs\ s\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
69 |
{\isaliteral{22}{\isachardoublequoteopen}}substs\ s\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{23}{\isacharhash}}\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ subst\ s\ t\ {\isaliteral{23}{\isacharhash}}\ substs\ s\ ts{\isaliteral{22}{\isachardoublequoteclose}}% |
|
8749 | 70 |
\begin{isamarkuptext}% |
71 |
\noindent |
|
11458 | 72 |
Individual equations in a \commdx{primrec} definition may be |
40406 | 73 |
named as shown for \isa{subst{\isaliteral{5F}{\isacharunderscore}}App}. |
10171 | 74 |
The significance of this device will become apparent below. |
9644 | 75 |
|
8749 | 76 |
Similarly, when proving a statement about terms inductively, we need |
77 |
to prove a related statement about term lists simultaneously. For example, |
|
78 |
the fact that the identity substitution does not change a term needs to be |
|
79 |
strengthened and proved as follows:% |
|
80 |
\end{isamarkuptext}% |
|
17175 | 81 |
\isamarkuptrue% |
82 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 83 |
\ subst{\isaliteral{5F}{\isacharunderscore}}id{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst\ \ Var\ t\ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline |
84 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}ts{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
17056 | 85 |
% |
86 |
\isadelimproof |
|
87 |
% |
|
88 |
\endisadelimproof |
|
89 |
% |
|
90 |
\isatagproof |
|
17175 | 91 |
\isacommand{apply}\isamarkupfalse% |
40406 | 92 |
{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ t\ \isakeyword{and}\ ts{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\isanewline |
17175 | 93 |
\isacommand{done}\isamarkupfalse% |
94 |
% |
|
17056 | 95 |
\endisatagproof |
96 |
{\isafoldproof}% |
|
97 |
% |
|
98 |
\isadelimproof |
|
99 |
% |
|
100 |
\endisadelimproof |
|
11866 | 101 |
% |
8749 | 102 |
\begin{isamarkuptext}% |
103 |
\noindent |
|
9933 | 104 |
Note that \isa{Var} is the identity substitution because by definition it |
40406 | 105 |
leaves variables unchanged: \isa{subst\ Var\ {\isaliteral{28}{\isacharparenleft}}Var\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ x}. Note also |
8749 | 106 |
that the type annotations are necessary because otherwise there is nothing in |
107 |
the goal to enforce that both halves of the goal talk about the same type |
|
40406 | 108 |
parameters \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}}. As a result, induction would fail |
8749 | 109 |
because the two halves of the goal would be unrelated. |
110 |
||
111 |
\begin{exercise} |
|
112 |
The fact that substitution distributes over composition can be expressed |
|
113 |
roughly as follows: |
|
9792 | 114 |
\begin{isabelle}% |
40406 | 115 |
\ \ \ \ \ subst\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ g{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ subst\ f\ {\isaliteral{28}{\isacharparenleft}}subst\ g\ t{\isaliteral{29}{\isacharparenright}}% |
9924 | 116 |
\end{isabelle} |
8749 | 117 |
Correct this statement (you will find that it does not type-check), |
40406 | 118 |
strengthen it, and prove it. (Note: \isa{{\isaliteral{5C3C636972633E}{\isasymcirc}}} is function composition; |
119 |
its definition is found in theorem \isa{o{\isaliteral{5F}{\isacharunderscore}}def}). |
|
8749 | 120 |
\end{exercise} |
9644 | 121 |
\begin{exercise}\label{ex:trev-trev} |
40406 | 122 |
Define a function \isa{trev} of type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}\ Nested{\isaliteral{2E}{\isachardot}}term\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}\ Nested{\isaliteral{2E}{\isachardot}}term} |
9792 | 123 |
that recursively reverses the order of arguments of all function symbols in a |
40406 | 124 |
term. Prove that \isa{trev\ {\isaliteral{28}{\isacharparenleft}}trev\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ t}. |
9644 | 125 |
\end{exercise} |
126 |
||
10795 | 127 |
The experienced functional programmer may feel that our definition of |
128 |
\isa{subst} is too complicated in that \isa{substs} is |
|
129 |
unnecessary. The \isa{App}-case can be defined directly as |
|
9644 | 130 |
\begin{isabelle}% |
40406 | 131 |
\ \ \ \ \ subst\ s\ {\isaliteral{28}{\isacharparenleft}}App\ f\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ f\ {\isaliteral{28}{\isacharparenleft}}map\ {\isaliteral{28}{\isacharparenleft}}subst\ s{\isaliteral{29}{\isacharparenright}}\ ts{\isaliteral{29}{\isacharparenright}}% |
9924 | 132 |
\end{isabelle} |
9644 | 133 |
where \isa{map} is the standard list function such that |
40406 | 134 |
\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2C}{\isacharcomma}}xn{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}f\ x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2C}{\isacharcomma}}f\ xn{\isaliteral{5D}{\isacharbrackright}}}. This is true, but Isabelle |
10795 | 135 |
insists on the conjunctive format. Fortunately, we can easily \emph{prove} |
9792 | 136 |
that the suggested equation holds:% |
9644 | 137 |
\end{isamarkuptext}% |
17175 | 138 |
\isamarkuptrue% |
17056 | 139 |
% |
140 |
\isadelimproof |
|
141 |
% |
|
142 |
\endisadelimproof |
|
143 |
% |
|
144 |
\isatagproof |
|
145 |
% |
|
146 |
\endisatagproof |
|
147 |
{\isafoldproof}% |
|
148 |
% |
|
149 |
\isadelimproof |
|
150 |
% |
|
151 |
\endisadelimproof |
|
152 |
% |
|
153 |
\isadelimproof |
|
154 |
% |
|
155 |
\endisadelimproof |
|
156 |
% |
|
157 |
\isatagproof |
|
17175 | 158 |
% |
159 |
\endisatagproof |
|
160 |
{\isafoldproof}% |
|
161 |
% |
|
162 |
\isadelimproof |
|
163 |
% |
|
164 |
\endisadelimproof |
|
165 |
% |
|
166 |
\isadelimproof |
|
167 |
% |
|
168 |
\endisadelimproof |
|
169 |
% |
|
170 |
\isatagproof |
|
171 |
% |
|
172 |
\endisatagproof |
|
173 |
{\isafoldproof}% |
|
174 |
% |
|
175 |
\isadelimproof |
|
176 |
\isanewline |
|
177 |
% |
|
178 |
\endisadelimproof |
|
179 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 180 |
\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst\ s\ {\isaliteral{28}{\isacharparenleft}}App\ f\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ f\ {\isaliteral{28}{\isacharparenleft}}map\ {\isaliteral{28}{\isacharparenleft}}subst\ s{\isaliteral{29}{\isacharparenright}}\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
17175 | 181 |
% |
182 |
\isadelimproof |
|
183 |
% |
|
184 |
\endisadelimproof |
|
185 |
% |
|
186 |
\isatagproof |
|
187 |
\isacommand{apply}\isamarkupfalse% |
|
40406 | 188 |
{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ ts{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\isanewline |
17175 | 189 |
\isacommand{done}\isamarkupfalse% |
17056 | 190 |
% |
191 |
\endisatagproof |
|
192 |
{\isafoldproof}% |
|
193 |
% |
|
194 |
\isadelimproof |
|
195 |
% |
|
196 |
\endisadelimproof |
|
197 |
% |
|
9644 | 198 |
\begin{isamarkuptext}% |
9689 | 199 |
\noindent |
9644 | 200 |
What is more, we can now disable the old defining equation as a |
201 |
simplification rule:% |
|
202 |
\end{isamarkuptext}% |
|
17175 | 203 |
\isamarkuptrue% |
204 |
\isacommand{declare}\isamarkupfalse% |
|
40406 | 205 |
\ subst{\isaliteral{5F}{\isacharunderscore}}App\ {\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}% |
9644 | 206 |
\begin{isamarkuptext}% |
25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25258
diff
changeset
|
207 |
\noindent The advantage is that now we have replaced \isa{substs} by \isa{map}, we can profit from the large number of |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25258
diff
changeset
|
208 |
pre-proved lemmas about \isa{map}. Unfortunately, inductive proofs |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25258
diff
changeset
|
209 |
about type \isa{term} are still awkward because they expect a |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25258
diff
changeset
|
210 |
conjunction. One could derive a new induction principle as well (see |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25258
diff
changeset
|
211 |
\S\ref{sec:derive-ind}), but simpler is to stop using |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25258
diff
changeset
|
212 |
\isacommand{primrec} and to define functions with \isacommand{fun} |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25258
diff
changeset
|
213 |
instead. Simple uses of \isacommand{fun} are described in |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25258
diff
changeset
|
214 |
\S\ref{sec:fun} below. Advanced applications, including functions |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25258
diff
changeset
|
215 |
over nested datatypes like \isa{term}, are discussed in a |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25258
diff
changeset
|
216 |
separate tutorial~\cite{isabelle-function}. |
8749 | 217 |
|
10971 | 218 |
Of course, you may also combine mutual and nested recursion of datatypes. For example, |
8749 | 219 |
constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of |
40406 | 220 |
expressions as its argument: \isa{Sum}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ aexp\ list{\isaliteral{22}{\isachardoublequote}}}.% |
8749 | 221 |
\end{isamarkuptext}% |
17175 | 222 |
\isamarkuptrue% |
17056 | 223 |
% |
224 |
\isadelimtheory |
|
225 |
% |
|
226 |
\endisadelimtheory |
|
227 |
% |
|
228 |
\isatagtheory |
|
229 |
% |
|
230 |
\endisatagtheory |
|
231 |
{\isafoldtheory}% |
|
232 |
% |
|
233 |
\isadelimtheory |
|
234 |
% |
|
235 |
\endisadelimtheory |
|
9722 | 236 |
\end{isabellebody}% |
9145 | 237 |
%%% Local Variables: |
238 |
%%% mode: latex |
|
239 |
%%% TeX-master: "root" |
|
240 |
%%% End: |