doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
changeset 25731 b3e415b0cf5c
parent 25056 743f3603ba8b
child 26318 967323f93c67
     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;