doc-src/Codegen/Thy/document/Adaptation.tex
changeset 38813 f50f0802ba99
parent 38509 9cea8a0e925a
child 39068 5ac590e8b320
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Fri Aug 27 14:22:33 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Fri Aug 27 14:24:26 2010 +0200
@@ -240,7 +240,7 @@
 \hspace*{0pt}structure Example :~sig\\
 \hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
 \hspace*{0pt} ~datatype boola = True | False\\
-\hspace*{0pt} ~val anda :~boola -> boola -> boola\\
+\hspace*{0pt} ~val conj :~boola -> boola -> boola\\
 \hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> boola\\
 \hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> boola\\
 \hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> boola\\
@@ -250,17 +250,17 @@
 \hspace*{0pt}\\
 \hspace*{0pt}datatype boola = True | False;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun anda p True = p\\
-\hspace*{0pt} ~| anda p False = False\\
-\hspace*{0pt} ~| anda True p = p\\
-\hspace*{0pt} ~| anda False p = False;\\
+\hspace*{0pt}fun conj p True = p\\
+\hspace*{0pt} ~| conj p False = False\\
+\hspace*{0pt} ~| conj True p = p\\
+\hspace*{0pt} ~| conj False p = False;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
 \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 = conj (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
 \hspace*{0pt}\\
 \hspace*{0pt}end;~(*struct Example*)%
 \end{isamarkuptext}%