3 \def\isabellecontext{Numbers}% |
3 \def\isabellecontext{Numbers}% |
4 \isanewline |
4 \isanewline |
5 \isacommand{theory}\ Numbers\ {\isacharequal}\ Real{\isacharcolon}\isanewline |
5 \isacommand{theory}\ Numbers\ {\isacharequal}\ Real{\isacharcolon}\isanewline |
6 \isanewline |
6 \isanewline |
7 \isamarkupfalse% |
7 \isamarkupfalse% |
8 \isacommand{ML}\ {\isachardoublequote}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequote}\isanewline |
8 \isamarkupfalse% |
9 \isamarkupfalse% |
9 \isamarkupfalse% |
10 \isacommand{ML}\ {\isachardoublequote}IsarOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isamarkupfalse% |
|
11 % |
10 % |
12 \begin{isamarkuptext}% |
11 \begin{isamarkuptext}% |
13 numeric literals; default simprules; can re-orient% |
12 numeric literals; default simprules; can re-orient% |
14 \end{isamarkuptext}% |
13 \end{isamarkuptext}% |
15 \isamarkuptrue% |
14 \isamarkuptrue% |
16 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequote}\isamarkupfalse% |
15 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequote}\isamarkupfalse% |
17 % |
16 \isamarkuptrue% |
18 \begin{isamarkuptxt}% |
17 \isanewline |
19 \begin{isabelle}% |
|
20 \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m% |
|
21 \end{isabelle}% |
|
22 \end{isamarkuptxt}% |
|
23 \isamarkuptrue% |
|
24 \isacommand{oops}\isanewline |
|
25 \isanewline |
18 \isanewline |
26 \isamarkupfalse% |
19 \isamarkupfalse% |
27 \isacommand{consts}\ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
20 \isacommand{consts}\ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
28 \isamarkupfalse% |
21 \isamarkupfalse% |
29 \isacommand{recdef}\ h\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline |
22 \isacommand{recdef}\ h\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline |
73 |
66 |
74 these form add_ac; similarly there is mult_ac% |
67 these form add_ac; similarly there is mult_ac% |
75 \end{isamarkuptext}% |
68 \end{isamarkuptext}% |
76 \isamarkuptrue% |
69 \isamarkuptrue% |
77 \isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}i\ {\isacharplus}\ j{\isacharasterisk}l{\isacharasterisk}k\ {\isacharplus}\ m{\isacharasterisk}n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n{\isacharasterisk}m\ {\isacharplus}\ i\ {\isacharplus}\ k{\isacharasterisk}j{\isacharasterisk}l{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
70 \isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}i\ {\isacharplus}\ j{\isacharasterisk}l{\isacharasterisk}k\ {\isacharplus}\ m{\isacharasterisk}n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n{\isacharasterisk}m\ {\isacharplus}\ i\ {\isacharplus}\ k{\isacharasterisk}j{\isacharasterisk}l{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
78 % |
71 \isamarkuptrue% |
79 \begin{isamarkuptxt}% |
72 \isamarkupfalse% |
80 \begin{isabelle}% |
73 \isamarkuptrue% |
81 \ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}% |
74 \isamarkupfalse% |
82 \end{isabelle}% |
|
83 \end{isamarkuptxt}% |
|
84 \isamarkuptrue% |
|
85 \isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ add{\isacharunderscore}ac\ mult{\isacharunderscore}ac{\isacharparenright}\isamarkupfalse% |
|
86 % |
|
87 \begin{isamarkuptxt}% |
|
88 \begin{isabelle}% |
|
89 \ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
|
90 \isaindent{\ {\isadigit{1}}{\isachardot}\ }f\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}% |
|
91 \end{isabelle}% |
|
92 \end{isamarkuptxt}% |
|
93 \isamarkuptrue% |
|
94 \isacommand{oops}\isamarkupfalse% |
|
95 % |
75 % |
96 \begin{isamarkuptext}% |
76 \begin{isamarkuptext}% |
97 \begin{isabelle}% |
77 \begin{isabelle}% |
98 m\ {\isasymle}\ n\ {\isasymLongrightarrow}\ m\ div\ k\ {\isasymle}\ n\ div\ k% |
78 m\ {\isasymle}\ n\ {\isasymLongrightarrow}\ m\ div\ k\ {\isasymle}\ n\ div\ k% |
99 \end{isabelle} |
79 \end{isabelle} |
115 \rulename{nat_diff_split}% |
95 \rulename{nat_diff_split}% |
116 \end{isamarkuptext}% |
96 \end{isamarkuptext}% |
117 \isamarkuptrue% |
97 \isamarkuptrue% |
118 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline |
98 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline |
119 \isamarkupfalse% |
99 \isamarkupfalse% |
120 \isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split\ iff\ del{\isacharcolon}\ less{\isacharunderscore}Suc{\isadigit{0}}{\isacharparenright}\isanewline |
100 \isamarkupfalse% |
121 \ % |
101 \isamarkupfalse% |
122 \isamarkupcmt{\begin{isabelle}% |
102 \isanewline |
123 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ Suc\ {\isadigit{0}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ Suc\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}% |
|
124 \end{isabelle}% |
|
125 } |
|
126 \isanewline |
|
127 \isamarkupfalse% |
|
128 \isacommand{apply}\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}n{\isacharequal}{\isadigit{0}}{\isachardoublequote}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline |
|
129 \isamarkupfalse% |
|
130 \isacommand{done}\isanewline |
|
131 \isanewline |
103 \isanewline |
132 \isanewline |
104 \isanewline |
133 \isamarkupfalse% |
105 \isamarkupfalse% |
134 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline |
106 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline |
135 \isamarkupfalse% |
107 \isamarkupfalse% |
136 \isacommand{apply}\ {\isacharparenleft}simp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharcomma}\ clarify{\isacharparenright}\isanewline |
108 \isamarkupfalse% |
137 \ % |
109 \isamarkupfalse% |
138 \isamarkupcmt{\begin{isabelle}% |
110 \isamarkupfalse% |
139 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ {\isadigit{4}}\ {\isacharplus}\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}% |
|
140 \end{isabelle}% |
|
141 } |
|
142 \isanewline |
|
143 \isamarkupfalse% |
|
144 \isacommand{apply}\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}n{\isacharequal}{\isadigit{0}}\ {\isacharbar}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline |
|
145 \isamarkupfalse% |
|
146 \isacommand{done}\isamarkupfalse% |
|
147 % |
111 % |
148 \begin{isamarkuptext}% |
112 \begin{isamarkuptext}% |
149 \begin{isabelle}% |
113 \begin{isabelle}% |
150 m\ mod\ n\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ m\ else\ {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ mod\ n{\isacharparenright}% |
114 m\ mod\ n\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ m\ else\ {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ mod\ n{\isacharparenright}% |
151 \end{isabelle} |
115 \end{isabelle} |
262 \rulename{zmod_zmult2_eq}% |
226 \rulename{zmod_zmult2_eq}% |
263 \end{isamarkuptext}% |
227 \end{isamarkuptext}% |
264 \isamarkuptrue% |
228 \isamarkuptrue% |
265 \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline |
229 \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline |
266 \isamarkupfalse% |
230 \isamarkupfalse% |
267 \isacommand{by}\ arith\isanewline |
231 \isanewline |
268 \isanewline |
232 \isanewline |
269 \isamarkupfalse% |
233 \isamarkupfalse% |
270 \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline |
234 \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline |
271 \isamarkupfalse% |
235 \isamarkupfalse% |
272 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
236 \isamarkupfalse% |
273 % |
237 % |
274 \begin{isamarkuptext}% |
238 \begin{isamarkuptext}% |
275 Induction rules for the Integers |
239 Induction rules for the Integers |
276 |
240 |
277 \begin{isabelle}% |
241 \begin{isabelle}% |
342 \rulename{add_divide_distrib}% |
306 \rulename{add_divide_distrib}% |
343 \end{isamarkuptext}% |
307 \end{isamarkuptext}% |
344 \isamarkuptrue% |
308 \isamarkuptrue% |
345 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{3}}{\isacharslash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isadigit{7}}{\isacharslash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline |
309 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{3}}{\isacharslash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isadigit{7}}{\isacharslash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline |
346 \isamarkupfalse% |
310 \isamarkupfalse% |
347 \isacommand{by}\ simp\ \isanewline |
|
348 \isanewline |
311 \isanewline |
349 \isamarkupfalse% |
312 \isamarkupfalse% |
350 \isacommand{lemma}\ {\isachardoublequote}P\ {\isacharparenleft}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
313 \isacommand{lemma}\ {\isachardoublequote}P\ {\isacharparenleft}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
351 % |
314 \isamarkuptrue% |
352 \begin{isamarkuptxt}% |
315 \isamarkupfalse% |
353 \begin{isabelle}% |
316 \isamarkuptrue% |
354 \ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}{\isacharparenright}% |
317 \isanewline |
355 \end{isabelle}% |
|
356 \end{isamarkuptxt}% |
|
357 \isamarkuptrue% |
|
358 \isacommand{apply}\ simp\isamarkupfalse% |
|
359 % |
|
360 \begin{isamarkuptxt}% |
|
361 \begin{isabelle}% |
|
362 \ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{2}}\ {\isacharslash}\ {\isadigit{5}}{\isacharparenright}% |
|
363 \end{isabelle}% |
|
364 \end{isamarkuptxt}% |
|
365 \isamarkuptrue% |
|
366 \isacommand{oops}\isanewline |
|
367 \isanewline |
318 \isanewline |
368 \isamarkupfalse% |
319 \isamarkupfalse% |
369 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
320 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
370 % |
321 \isamarkuptrue% |
371 \begin{isamarkuptxt}% |
322 \isamarkupfalse% |
372 \begin{isabelle}% |
323 \isamarkuptrue% |
373 \ {\isadigit{1}}{\isachardot}\ {\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ x% |
324 \isanewline |
374 \end{isabelle}% |
|
375 \end{isamarkuptxt}% |
|
376 \isamarkuptrue% |
|
377 \isacommand{apply}\ simp\isamarkupfalse% |
|
378 % |
|
379 \begin{isamarkuptxt}% |
|
380 \begin{isabelle}% |
|
381 \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharless}\ x\ {\isacharasterisk}\ {\isadigit{5}}% |
|
382 \end{isabelle}% |
|
383 \end{isamarkuptxt}% |
|
384 \isamarkuptrue% |
|
385 \isacommand{oops}\isanewline |
|
386 \isanewline |
325 \isanewline |
387 \isamarkupfalse% |
326 \isamarkupfalse% |
388 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcircum}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline |
327 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcircum}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline |
389 \isamarkupfalse% |
328 \isamarkupfalse% |
390 \isacommand{apply}\ simp\ \isanewline |
329 \isamarkupfalse% |
391 \isamarkupfalse% |
330 \isamarkupfalse% |
392 \isacommand{oops}\isamarkupfalse% |
|
393 % |
331 % |
394 \begin{isamarkuptext}% |
332 \begin{isamarkuptext}% |
395 Ring and Field |
333 Ring and Field |
396 |
334 |
397 Requires a field, or else an ordered ring |
335 Requires a field, or else an ordered ring |
415 {\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% |
353 {\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% |
416 \end{isabelle} |
354 \end{isabelle} |
417 \rulename{field_mult_cancel_right}% |
355 \rulename{field_mult_cancel_right}% |
418 \end{isamarkuptext}% |
356 \end{isamarkuptext}% |
419 \isamarkuptrue% |
357 \isamarkuptrue% |
420 \isacommand{ML}{\isacharbraceleft}{\isacharasterisk}set\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}\isamarkupfalse% |
358 \isamarkupfalse% |
421 % |
359 % |
422 \begin{isamarkuptext}% |
360 \begin{isamarkuptext}% |
423 effect of show sorts on the above |
361 effect of show sorts on the above |
424 |
362 |
425 \begin{isabelle}% |
363 \begin{isabelle}% |