--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML Sat Nov 04 19:25:39 2006 +0100
@@ -11,8 +11,8 @@
fun op_conj y True = y
| op_conj x False = False
- | op_conj True ya = ya
- | op_conj False xa = False;
+ | op_conj True y = y
+ | op_conj False x = False;
end; (*struct HOL*)
@@ -22,8 +22,8 @@
datatype nat = Zero_nat | Succ_nat of nat;
fun less_nat Zero_nat (Succ_nat n) = HOL.True
- | less_nat na Zero_nat = HOL.False
- | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
+ | less_nat n Zero_nat = HOL.False
+ | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
fun less_eq_nat m n = HOL.nota (less_nat n m);