|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Typedefs}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsection{Introducing New Types% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \begin{isamarkuptext}% |
|
11 \label{sec:adv-typedef} |
|
12 For most applications, a combination of predefined types like \isa{bool} and |
|
13 \isa{{\isasymRightarrow}} with recursive datatypes and records is quite sufficient. Very |
|
14 occasionally you may feel the need for a more advanced type. If you |
|
15 are certain that your type is not definable by any of the |
|
16 standard means, then read on. |
|
17 \begin{warn} |
|
18 Types in HOL must be non-empty; otherwise the quantifier rules would be |
|
19 unsound, because $\exists x.\ x=x$ is a theorem. |
|
20 \end{warn}% |
|
21 \end{isamarkuptext}% |
|
22 \isamarkuptrue% |
|
23 % |
|
24 \isamarkupsubsection{Declaring New Types% |
|
25 } |
|
26 \isamarkuptrue% |
|
27 % |
|
28 \begin{isamarkuptext}% |
|
29 \label{sec:typedecl} |
|
30 \index{types!declaring|(}% |
|
31 \index{typedecl@\isacommand {typedecl} (command)}% |
|
32 The most trivial way of introducing a new type is by a \textbf{type |
|
33 declaration}:% |
|
34 \end{isamarkuptext}% |
|
35 \isamarkuptrue% |
|
36 \isacommand{typedecl}\ my{\isacharunderscore}new{\isacharunderscore}type\isamarkupfalse% |
|
37 % |
|
38 \begin{isamarkuptext}% |
|
39 \noindent |
|
40 This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its |
|
41 name. Thus we know nothing about this type, except that it is |
|
42 non-empty. Such declarations without definitions are |
|
43 useful if that type can be viewed as a parameter of the theory. |
|
44 A typical example is given in \S\ref{sec:VMC}, where we define a transition |
|
45 relation over an arbitrary type of states. |
|
46 |
|
47 In principle we can always get rid of such type declarations by making those |
|
48 types parameters of every other type, thus keeping the theory generic. In |
|
49 practice, however, the resulting clutter can make types hard to read. |
|
50 |
|
51 If you are looking for a quick and dirty way of introducing a new type |
|
52 together with its properties: declare the type and state its properties as |
|
53 axioms. Example:% |
|
54 \end{isamarkuptext}% |
|
55 \isamarkuptrue% |
|
56 \isacommand{axioms}\isanewline |
|
57 just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ {\isasymforall}y{\isachardot}\ x\ {\isacharequal}\ y{\isachardoublequote}\isamarkupfalse% |
|
58 % |
|
59 \begin{isamarkuptext}% |
|
60 \noindent |
|
61 However, we strongly discourage this approach, except at explorative stages |
|
62 of your development. It is extremely easy to write down contradictory sets of |
|
63 axioms, in which case you will be able to prove everything but it will mean |
|
64 nothing. In the example above, the axiomatic approach is |
|
65 unnecessary: a one-element type called \isa{unit} is already defined in HOL. |
|
66 \index{types!declaring|)}% |
|
67 \end{isamarkuptext}% |
|
68 \isamarkuptrue% |
|
69 % |
|
70 \isamarkupsubsection{Defining New Types% |
|
71 } |
|
72 \isamarkuptrue% |
|
73 % |
|
74 \begin{isamarkuptext}% |
|
75 \label{sec:typedef} |
|
76 \index{types!defining|(}% |
|
77 \index{typedecl@\isacommand {typedef} (command)|(}% |
|
78 Now we come to the most general means of safely introducing a new type, the |
|
79 \textbf{type definition}. All other means, for example |
|
80 \isacommand{datatype}, are based on it. The principle is extremely simple: |
|
81 any non-empty subset of an existing type can be turned into a new type. Thus |
|
82 a type definition is merely a notational device: you introduce a new name for |
|
83 a subset of an existing type. This does not add any logical power to HOL, |
|
84 because you could base all your work directly on the subset of the existing |
|
85 type. However, the resulting theories could easily become indigestible |
|
86 because instead of implicit types you would have explicit sets in your |
|
87 formulae. |
|
88 |
|
89 Let us work a simple example, the definition of a three-element type. |
|
90 It is easily represented by the first three natural numbers:% |
|
91 \end{isamarkuptext}% |
|
92 \isamarkuptrue% |
|
93 \isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse% |
|
94 % |
|
95 \begin{isamarkuptxt}% |
|
96 \noindent |
|
97 In order to enforce that the representing set on the right-hand side is |
|
98 non-empty, this definition actually starts a proof to that effect: |
|
99 \begin{isabelle}% |
|
100 \ {\isadigit{1}}{\isachardot}\ {\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}% |
|
101 \end{isabelle} |
|
102 Fortunately, this is easy enough to show: take 0 as a witness.% |
|
103 \end{isamarkuptxt}% |
|
104 \isamarkuptrue% |
|
105 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isadigit{0}}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline |
|
106 \isamarkupfalse% |
|
107 \isacommand{by}\ simp\isamarkupfalse% |
|
108 % |
|
109 \begin{isamarkuptext}% |
|
110 This type definition introduces the new type \isa{three} and asserts |
|
111 that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharbraceright}}. This assertion |
|
112 is expressed via a bijection between the \emph{type} \isa{three} and the |
|
113 \emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharbraceright}}. To this end, the command declares the following |
|
114 constants behind the scenes: |
|
115 \begin{center} |
|
116 \begin{tabular}{rcl} |
|
117 \isa{three} &::& \isa{nat\ set} \\ |
|
118 \isa{Rep{\isacharunderscore}three} &::& \isa{three\ {\isasymRightarrow}\ nat}\\ |
|
119 \isa{Abs{\isacharunderscore}three} &::& \isa{nat\ {\isasymRightarrow}\ three} |
|
120 \end{tabular} |
|
121 \end{center} |
|
122 where constant \isa{three} is explicitly defined as the representing set: |
|
123 \begin{center} |
|
124 \isa{three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def}) |
|
125 \end{center} |
|
126 The situation is best summarized with the help of the following diagram, |
|
127 where squares are types and circles are sets: |
|
128 \begin{center} |
|
129 \unitlength1mm |
|
130 \thicklines |
|
131 \begin{picture}(100,40) |
|
132 \put(3,13){\framebox(15,15){\isa{three}}} |
|
133 \put(55,5){\framebox(30,30){\isa{three}}} |
|
134 \put(70,32){\makebox(0,0){\isa{nat}}} |
|
135 \put(70,20){\circle{40}} |
|
136 \put(10,15){\vector(1,0){60}} |
|
137 \put(25,14){\makebox(0,0)[tl]{\isa{Rep{\isacharunderscore}three}}} |
|
138 \put(70,25){\vector(-1,0){60}} |
|
139 \put(25,26){\makebox(0,0)[bl]{\isa{Abs{\isacharunderscore}three}}} |
|
140 \end{picture} |
|
141 \end{center} |
|
142 Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is |
|
143 surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other: |
|
144 \begin{center} |
|
145 \begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}} |
|
146 \isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} & (\isa{Rep{\isacharunderscore}three}) \\ |
|
147 \isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\ |
|
148 \isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse}) |
|
149 \end{tabular} |
|
150 \end{center} |
|
151 % |
|
152 From this example it should be clear what \isacommand{typedef} does |
|
153 in general given a name (here \isa{three}) and a set |
|
154 (here \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharbraceright}}). |
|
155 |
|
156 Our next step is to define the basic functions expected on the new type. |
|
157 Although this depends on the type at hand, the following strategy works well: |
|
158 \begin{itemize} |
|
159 \item define a small kernel of basic functions that can express all other |
|
160 functions you anticipate. |
|
161 \item define the kernel in terms of corresponding functions on the |
|
162 representing type using \isa{Abs} and \isa{Rep} to convert between the |
|
163 two levels. |
|
164 \end{itemize} |
|
165 In our example it suffices to give the three elements of type \isa{three} |
|
166 names:% |
|
167 \end{isamarkuptext}% |
|
168 \isamarkuptrue% |
|
169 \isacommand{constdefs}\isanewline |
|
170 \ \ A{\isacharcolon}{\isacharcolon}\ three\isanewline |
|
171 \ {\isachardoublequote}A\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{0}}{\isachardoublequote}\isanewline |
|
172 \ \ B{\isacharcolon}{\isacharcolon}\ three\isanewline |
|
173 \ {\isachardoublequote}B\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{1}}{\isachardoublequote}\isanewline |
|
174 \ \ C\ {\isacharcolon}{\isacharcolon}\ three\isanewline |
|
175 \ {\isachardoublequote}C\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{2}}{\isachardoublequote}\isamarkupfalse% |
|
176 % |
|
177 \begin{isamarkuptext}% |
|
178 So far, everything was easy. But it is clear that reasoning about \isa{three} will be hell if we have to go back to \isa{nat} every time. Thus our |
|
179 aim must be to raise our level of abstraction by deriving enough theorems |
|
180 about type \isa{three} to characterize it completely. And those theorems |
|
181 should be phrased in terms of \isa{A}, \isa{B} and \isa{C}, not \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three}. Because of the simplicity of the example, |
|
182 we merely need to prove that \isa{A}, \isa{B} and \isa{C} are distinct |
|
183 and that they exhaust the type. |
|
184 |
|
185 In processing our \isacommand{typedef} declaration, |
|
186 Isabelle helpfully proves several lemmas. |
|
187 One, \isa{Abs{\isacharunderscore}three{\isacharunderscore}inject}, |
|
188 expresses that \isa{Abs{\isacharunderscore}three} is injective on the representing subset: |
|
189 \begin{center} |
|
190 \isa{{\isasymlbrakk}x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}} |
|
191 \end{center} |
|
192 Another, \isa{Rep{\isacharunderscore}three{\isacharunderscore}inject}, expresses that the representation |
|
193 function is also injective: |
|
194 \begin{center} |
|
195 \isa{{\isacharparenleft}Rep{\isacharunderscore}three\ x\ {\isacharequal}\ Rep{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}} |
|
196 \end{center} |
|
197 Distinctness of \isa{A}, \isa{B} and \isa{C} follows immediately |
|
198 if we expand their definitions and rewrite with the injectivity |
|
199 of \isa{Abs{\isacharunderscore}three}:% |
|
200 \end{isamarkuptext}% |
|
201 \isamarkuptrue% |
|
202 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymnoteq}\ B\ {\isasymand}\ B\ {\isasymnoteq}\ A\ {\isasymand}\ A\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ A\ {\isasymand}\ B\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ B{\isachardoublequote}\isanewline |
|
203 \isamarkupfalse% |
|
204 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}inject\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ three{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
|
205 % |
|
206 \begin{isamarkuptext}% |
|
207 \noindent |
|
208 Of course we rely on the simplifier to solve goals like \isa{{\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}}. |
|
209 |
|
210 The fact that \isa{A}, \isa{B} and \isa{C} exhaust type \isa{three} is |
|
211 best phrased as a case distinction theorem: if you want to prove \isa{P\ x} |
|
212 (where \isa{x} is of type \isa{three}) it suffices to prove \isa{P\ A}, |
|
213 \isa{P\ B} and \isa{P\ C}. First we prove the analogous proposition for the |
|
214 representation:% |
|
215 \end{isamarkuptext}% |
|
216 \isamarkuptrue% |
|
217 \isacommand{lemma}\ cases{\isacharunderscore}lemma{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ Q\ {\isadigit{0}}{\isacharsemicolon}\ Q\ {\isadigit{1}}{\isacharsemicolon}\ Q\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isasymin}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \ Q\ n{\isachardoublequote}\isamarkupfalse% |
|
218 % |
|
219 \begin{isamarkuptxt}% |
|
220 \noindent |
|
221 Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated |
|
222 elimination with \isa{le{\isacharunderscore}SucE} |
|
223 \begin{isabelle}% |
|
224 {\isasymlbrakk}{\isacharquery}m\ {\isasymle}\ Suc\ {\isacharquery}n{\isacharsemicolon}\ {\isacharquery}m\ {\isasymle}\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharsemicolon}\ {\isacharquery}m\ {\isacharequal}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R% |
|
225 \end{isabelle} |
|
226 reduces \isa{n\ {\isasymle}\ {\isadigit{2}}} to the three cases \isa{n\ {\isasymle}\ {\isadigit{0}}}, \isa{n\ {\isacharequal}\ {\isadigit{1}}} and |
|
227 \isa{n\ {\isacharequal}\ {\isadigit{2}}} which are trivial for simplification:% |
|
228 \end{isamarkuptxt}% |
|
229 \isamarkuptrue% |
|
230 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ numerals{\isacharparenright}\isanewline |
|
231 \isamarkupfalse% |
|
232 \isacommand{apply}{\isacharparenleft}{\isacharparenleft}erule\ le{\isacharunderscore}SucE{\isacharparenright}{\isacharplus}{\isacharparenright}\isanewline |
|
233 \isamarkupfalse% |
|
234 \isacommand{apply}\ simp{\isacharunderscore}all\isanewline |
|
235 \isamarkupfalse% |
|
236 \isacommand{done}\isamarkupfalse% |
|
237 % |
|
238 \begin{isamarkuptext}% |
|
239 Now the case distinction lemma on type \isa{three} is easy to derive if you |
|
240 know how:% |
|
241 \end{isamarkuptext}% |
|
242 \isamarkuptrue% |
|
243 \isacommand{lemma}\ three{\isacharunderscore}cases{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}\isamarkupfalse% |
|
244 % |
|
245 \begin{isamarkuptxt}% |
|
246 \noindent |
|
247 We start by replacing the \isa{x} by \isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}}:% |
|
248 \end{isamarkuptxt}% |
|
249 \isamarkuptrue% |
|
250 \isacommand{apply}{\isacharparenleft}rule\ subst{\isacharbrackleft}OF\ Rep{\isacharunderscore}three{\isacharunderscore}inverse{\isacharbrackright}{\isacharparenright}\isamarkupfalse% |
|
251 % |
|
252 \begin{isamarkuptxt}% |
|
253 \noindent |
|
254 This substitution step worked nicely because there was just a single |
|
255 occurrence of a term of type \isa{three}, namely \isa{x}. |
|
256 When we now apply \isa{cases{\isacharunderscore}lemma}, \isa{Q} becomes \isa{{\isasymlambda}n{\isachardot}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ n{\isacharparenright}} because \isa{Rep{\isacharunderscore}three\ x} is the only term of type \isa{nat}:% |
|
257 \end{isamarkuptxt}% |
|
258 \isamarkuptrue% |
|
259 \isacommand{apply}{\isacharparenleft}rule\ cases{\isacharunderscore}lemma{\isacharparenright}\isamarkupfalse% |
|
260 % |
|
261 \begin{isamarkuptxt}% |
|
262 \begin{isabelle}% |
|
263 \ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{0}}{\isacharparenright}\isanewline |
|
264 \ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{1}}{\isacharparenright}\isanewline |
|
265 \ {\isadigit{3}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{2}}{\isacharparenright}\isanewline |
|
266 \ {\isadigit{4}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ x\ {\isasymin}\ three% |
|
267 \end{isabelle} |
|
268 The resulting subgoals are easily solved by simplification:% |
|
269 \end{isamarkuptxt}% |
|
270 \isamarkuptrue% |
|
271 \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ Rep{\isacharunderscore}three{\isacharparenright}\isanewline |
|
272 \isamarkupfalse% |
|
273 \isacommand{done}\isamarkupfalse% |
|
274 % |
|
275 \begin{isamarkuptext}% |
|
276 \noindent |
|
277 This concludes the derivation of the characteristic theorems for |
|
278 type \isa{three}. |
|
279 |
|
280 The attentive reader has realized long ago that the |
|
281 above lengthy definition can be collapsed into one line:% |
|
282 \end{isamarkuptext}% |
|
283 \isamarkuptrue% |
|
284 \isacommand{datatype}\ three{\isacharprime}\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isamarkupfalse% |
|
285 % |
|
286 \begin{isamarkuptext}% |
|
287 \noindent |
|
288 In fact, the \isacommand{datatype} command performs internally more or less |
|
289 the same derivations as we did, which gives you some idea what life would be |
|
290 like without \isacommand{datatype}. |
|
291 |
|
292 Although \isa{three} could be defined in one line, we have chosen this |
|
293 example to demonstrate \isacommand{typedef} because its simplicity makes the |
|
294 key concepts particularly easy to grasp. If you would like to see a |
|
295 non-trivial example that cannot be defined more directly, we recommend the |
|
296 definition of \emph{finite multisets} in the HOL Library. |
|
297 |
|
298 Let us conclude by summarizing the above procedure for defining a new type. |
|
299 Given some abstract axiomatic description $P$ of a type $ty$ in terms of a |
|
300 set of functions $F$, this involves three steps: |
|
301 \begin{enumerate} |
|
302 \item Find an appropriate type $\tau$ and subset $A$ which has the desired |
|
303 properties $P$, and make a type definition based on this representation. |
|
304 \item Define the required functions $F$ on $ty$ by lifting |
|
305 analogous functions on the representation via $Abs_ty$ and $Rep_ty$. |
|
306 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation. |
|
307 \end{enumerate} |
|
308 You can now forget about the representation and work solely in terms of the |
|
309 abstract functions $F$ and properties $P$.% |
|
310 \index{typedecl@\isacommand {typedef} (command)|)}% |
|
311 \index{types!defining|)}% |
|
312 \end{isamarkuptext}% |
|
313 \isamarkuptrue% |
|
314 \isamarkupfalse% |
|
315 \end{isabellebody}% |
|
316 %%% Local Variables: |
|
317 %%% mode: latex |
|
318 %%% TeX-master: "root" |
|
319 %%% End: |