--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Thu Jan 01 21:28:38 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Thu Jan 01 21:30:13 2009 +0100
@@ -281,9 +281,9 @@
\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k, l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
\hspace*{0pt}\\
-\hspace*{0pt}end; (*struct Example*)%
+\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -357,9 +357,9 @@
\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k, l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
\hspace*{0pt}\\
-\hspace*{0pt}end; (*struct Example*)%
+\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -414,9 +414,9 @@
\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k, l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
+\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
\hspace*{0pt}\\
-\hspace*{0pt}end; (*struct Example*)%
+\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
\isamarkuptrue%
%