doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
changeset 28714 1992553cccfe
parent 28679 d7384e8e99b3
child 28727 185110a4b97a
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 31 10:39:04 2008 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Mon Nov 03 14:15:25 2008 +0100
     1.3 @@ -264,26 +264,26 @@
     1.4  \begin{isamarkuptext}%
     1.5  \isaverbatim%
     1.6  \noindent%
     1.7 -\verb|structure Example = |\newline%
     1.8 -\verb|struct|\newline%
     1.9 -\newline%
    1.10 -\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
    1.11 -\newline%
    1.12 -\verb|datatype boola = False |\verb,|,\verb| True;|\newline%
    1.13 -\newline%
    1.14 -\verb|fun anda x True = x|\newline%
    1.15 -\verb|  |\verb,|,\verb| anda x False = False|\newline%
    1.16 -\verb|  |\verb,|,\verb| anda True x = x|\newline%
    1.17 -\verb|  |\verb,|,\verb| anda False x = False;|\newline%
    1.18 -\newline%
    1.19 -\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
    1.20 -\verb|  |\verb,|,\verb| less_nat n Zero_nat = False|\newline%
    1.21 -\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
    1.22 -\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = True;|\newline%
    1.23 -\newline%
    1.24 -\verb|fun in_interval (k, l) n = anda (less_eq_nat k n) (less_eq_nat n l);|\newline%
    1.25 -\newline%
    1.26 -\verb|end; (*struct Example*)|%
    1.27 +\hspace*{0pt}structure Example = \\
    1.28 +\hspace*{0pt}struct\\
    1.29 +\hspace*{0pt}\\
    1.30 +\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    1.31 +\hspace*{0pt}\\
    1.32 +\hspace*{0pt}datatype boola = False | True;\\
    1.33 +\hspace*{0pt}\\
    1.34 +\hspace*{0pt}fun anda x True = x\\
    1.35 +\hspace*{0pt} ~| anda x False = False\\
    1.36 +\hspace*{0pt} ~| anda True x = x\\
    1.37 +\hspace*{0pt} ~| anda False x = False;\\
    1.38 +\hspace*{0pt}\\
    1.39 +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
    1.40 +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
    1.41 +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
    1.42 +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
    1.43 +\hspace*{0pt}\\
    1.44 +\hspace*{0pt}fun in{\char95}interval (k, l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
    1.45 +\hspace*{0pt}\\
    1.46 +\hspace*{0pt}end; (*struct Example*)%
    1.47  \end{isamarkuptext}%
    1.48  \isamarkuptrue%
    1.49  %
    1.50 @@ -347,19 +347,19 @@
    1.51  \begin{isamarkuptext}%
    1.52  \isaverbatim%
    1.53  \noindent%
    1.54 -\verb|structure Example = |\newline%
    1.55 -\verb|struct|\newline%
    1.56 -\newline%
    1.57 -\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
    1.58 -\newline%
    1.59 -\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
    1.60 -\verb|  |\verb,|,\verb| less_nat n Zero_nat = false|\newline%
    1.61 -\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
    1.62 -\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline%
    1.63 -\newline%
    1.64 -\verb|fun in_interval (k, l) n = (less_eq_nat k n) andalso (less_eq_nat n l);|\newline%
    1.65 -\newline%
    1.66 -\verb|end; (*struct Example*)|%
    1.67 +\hspace*{0pt}structure Example = \\
    1.68 +\hspace*{0pt}struct\\
    1.69 +\hspace*{0pt}\\
    1.70 +\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    1.71 +\hspace*{0pt}\\
    1.72 +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
    1.73 +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
    1.74 +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
    1.75 +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
    1.76 +\hspace*{0pt}\\
    1.77 +\hspace*{0pt}fun in{\char95}interval (k, l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
    1.78 +\hspace*{0pt}\\
    1.79 +\hspace*{0pt}end; (*struct Example*)%
    1.80  \end{isamarkuptext}%
    1.81  \isamarkuptrue%
    1.82  %
    1.83 @@ -404,19 +404,19 @@
    1.84  \begin{isamarkuptext}%
    1.85  \isaverbatim%
    1.86  \noindent%
    1.87 -\verb|structure Example = |\newline%
    1.88 -\verb|struct|\newline%
    1.89 -\newline%
    1.90 -\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
    1.91 -\newline%
    1.92 -\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
    1.93 -\verb|  |\verb,|,\verb| less_nat n Zero_nat = false|\newline%
    1.94 -\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
    1.95 -\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline%
    1.96 -\newline%
    1.97 -\verb|fun in_interval (k, l) n = less_eq_nat k n andalso less_eq_nat n l;|\newline%
    1.98 -\newline%
    1.99 -\verb|end; (*struct Example*)|%
   1.100 +\hspace*{0pt}structure Example = \\
   1.101 +\hspace*{0pt}struct\\
   1.102 +\hspace*{0pt}\\
   1.103 +\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
   1.104 +\hspace*{0pt}\\
   1.105 +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
   1.106 +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
   1.107 +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
   1.108 +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
   1.109 +\hspace*{0pt}\\
   1.110 +\hspace*{0pt}fun in{\char95}interval (k, l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
   1.111 +\hspace*{0pt}\\
   1.112 +\hspace*{0pt}end; (*struct Example*)%
   1.113  \end{isamarkuptext}%
   1.114  \isamarkuptrue%
   1.115  %
   1.116 @@ -533,7 +533,7 @@
   1.117  \isatagquotett
   1.118  \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
   1.119  \ eq\isanewline
   1.120 -\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}HOL{\isachardot}eq{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.121 +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.122  \isanewline
   1.123  \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   1.124  \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline