262 \isatagquote |
262 \isatagquote |
263 % |
263 % |
264 \begin{isamarkuptext}% |
264 \begin{isamarkuptext}% |
265 \isaverbatim% |
265 \isaverbatim% |
266 \noindent% |
266 \noindent% |
267 \verb|structure Example = |\newline% |
267 \hspace*{0pt}structure Example = \\ |
268 \verb|struct|\newline% |
268 \hspace*{0pt}struct\\ |
269 \newline% |
269 \hspace*{0pt}\\ |
270 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% |
270 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
271 \newline% |
271 \hspace*{0pt}\\ |
272 \verb|datatype boola = False |\verb,|,\verb| True;|\newline% |
272 \hspace*{0pt}datatype boola = False | True;\\ |
273 \newline% |
273 \hspace*{0pt}\\ |
274 \verb|fun anda x True = x|\newline% |
274 \hspace*{0pt}fun anda x True = x\\ |
275 \verb| |\verb,|,\verb| anda x False = False|\newline% |
275 \hspace*{0pt} ~| anda x False = False\\ |
276 \verb| |\verb,|,\verb| anda True x = x|\newline% |
276 \hspace*{0pt} ~| anda True x = x\\ |
277 \verb| |\verb,|,\verb| anda False x = False;|\newline% |
277 \hspace*{0pt} ~| anda False x = False;\\ |
278 \newline% |
278 \hspace*{0pt}\\ |
279 \verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline% |
279 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ |
280 \verb| |\verb,|,\verb| less_nat n Zero_nat = False|\newline% |
280 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\ |
281 \verb|and less_eq_nat (Suc m) n = less_nat m n|\newline% |
281 \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ |
282 \verb| |\verb,|,\verb| less_eq_nat Zero_nat n = True;|\newline% |
282 \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\ |
283 \newline% |
283 \hspace*{0pt}\\ |
284 \verb|fun in_interval (k, l) n = anda (less_eq_nat k n) (less_eq_nat n l);|\newline% |
284 \hspace*{0pt}fun in{\char95}interval (k, l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\ |
285 \newline% |
285 \hspace*{0pt}\\ |
286 \verb|end; (*struct Example*)|% |
286 \hspace*{0pt}end; (*struct Example*)% |
287 \end{isamarkuptext}% |
287 \end{isamarkuptext}% |
288 \isamarkuptrue% |
288 \isamarkuptrue% |
289 % |
289 % |
290 \endisatagquote |
290 \endisatagquote |
291 {\isafoldquote}% |
291 {\isafoldquote}% |
345 \isatagquote |
345 \isatagquote |
346 % |
346 % |
347 \begin{isamarkuptext}% |
347 \begin{isamarkuptext}% |
348 \isaverbatim% |
348 \isaverbatim% |
349 \noindent% |
349 \noindent% |
350 \verb|structure Example = |\newline% |
350 \hspace*{0pt}structure Example = \\ |
351 \verb|struct|\newline% |
351 \hspace*{0pt}struct\\ |
352 \newline% |
352 \hspace*{0pt}\\ |
353 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% |
353 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
354 \newline% |
354 \hspace*{0pt}\\ |
355 \verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline% |
355 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ |
356 \verb| |\verb,|,\verb| less_nat n Zero_nat = false|\newline% |
356 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\ |
357 \verb|and less_eq_nat (Suc m) n = less_nat m n|\newline% |
357 \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ |
358 \verb| |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline% |
358 \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\ |
359 \newline% |
359 \hspace*{0pt}\\ |
360 \verb|fun in_interval (k, l) n = (less_eq_nat k n) andalso (less_eq_nat n l);|\newline% |
360 \hspace*{0pt}fun in{\char95}interval (k, l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\ |
361 \newline% |
361 \hspace*{0pt}\\ |
362 \verb|end; (*struct Example*)|% |
362 \hspace*{0pt}end; (*struct Example*)% |
363 \end{isamarkuptext}% |
363 \end{isamarkuptext}% |
364 \isamarkuptrue% |
364 \isamarkuptrue% |
365 % |
365 % |
366 \endisatagquote |
366 \endisatagquote |
367 {\isafoldquote}% |
367 {\isafoldquote}% |
402 \isatagquote |
402 \isatagquote |
403 % |
403 % |
404 \begin{isamarkuptext}% |
404 \begin{isamarkuptext}% |
405 \isaverbatim% |
405 \isaverbatim% |
406 \noindent% |
406 \noindent% |
407 \verb|structure Example = |\newline% |
407 \hspace*{0pt}structure Example = \\ |
408 \verb|struct|\newline% |
408 \hspace*{0pt}struct\\ |
409 \newline% |
409 \hspace*{0pt}\\ |
410 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% |
410 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\ |
411 \newline% |
411 \hspace*{0pt}\\ |
412 \verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline% |
412 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ |
413 \verb| |\verb,|,\verb| less_nat n Zero_nat = false|\newline% |
413 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\ |
414 \verb|and less_eq_nat (Suc m) n = less_nat m n|\newline% |
414 \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ |
415 \verb| |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline% |
415 \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\ |
416 \newline% |
416 \hspace*{0pt}\\ |
417 \verb|fun in_interval (k, l) n = less_eq_nat k n andalso less_eq_nat n l;|\newline% |
417 \hspace*{0pt}fun in{\char95}interval (k, l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\ |
418 \newline% |
418 \hspace*{0pt}\\ |
419 \verb|end; (*struct Example*)|% |
419 \hspace*{0pt}end; (*struct Example*)% |
420 \end{isamarkuptext}% |
420 \end{isamarkuptext}% |
421 \isamarkuptrue% |
421 \isamarkuptrue% |
422 % |
422 % |
423 \endisatagquote |
423 \endisatagquote |
424 {\isafoldquote}% |
424 {\isafoldquote}% |
531 \endisadelimquotett |
531 \endisadelimquotett |
532 % |
532 % |
533 \isatagquotett |
533 \isatagquotett |
534 \isacommand{code{\isacharunderscore}class}\isamarkupfalse% |
534 \isacommand{code{\isacharunderscore}class}\isamarkupfalse% |
535 \ eq\isanewline |
535 \ eq\isanewline |
536 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}HOL{\isachardot}eq{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
536 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline |
537 \isanewline |
537 \isanewline |
538 \isacommand{code{\isacharunderscore}const}\isamarkupfalse% |
538 \isacommand{code{\isacharunderscore}const}\isamarkupfalse% |
539 \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline |
539 \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline |
540 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}% |
540 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}% |
541 \endisatagquotett |
541 \endisatagquotett |