1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Thu Dec 20 14:33:43 2007 +0100
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Thu Dec 20 21:09:38 2007 +0100
1.3 @@ -3,10 +3,10 @@
1.4
1.5 datatype nat = Suc of nat | Zero_nat;
1.6
1.7 -fun eqop_nat Zero_nat (Suc m) = false
1.8 - | eqop_nat (Suc n) Zero_nat = false
1.9 - | eqop_nat (Suc n) (Suc m) = eqop_nat n m
1.10 - | eqop_nat Zero_nat Zero_nat = true;
1.11 +fun eqop_nat Zero_nat Zero_nat = true
1.12 + | eqop_nat (Suc m) (Suc n) = eqop_nat m n
1.13 + | eqop_nat Zero_nat (Suc a) = false
1.14 + | eqop_nat (Suc a) Zero_nat = false;
1.15
1.16 fun plus_nat (Suc m) n = plus_nat m (Suc n)
1.17 | plus_nat Zero_nat n = n;