doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
changeset 21993 4b802a9e0738
parent 21341 3844037a8e2d
child 21994 dfa5133dbe73
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jan 04 15:29:44 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jan 04 17:11:09 2007 +0100
     1.3 @@ -4,8 +4,7 @@
     1.4  structure HOL = 
     1.5  struct
     1.6  
     1.7 -fun nota false = true
     1.8 -  | nota true = false;
     1.9 +fun nota false = true;
    1.10  
    1.11  end; (*struct HOL*)
    1.12  
    1.13 @@ -14,9 +13,7 @@
    1.14  
    1.15  datatype nat = Zero_nat | Suc of nat;
    1.16  
    1.17 -fun less_nat Zero_nat (Suc n) = true
    1.18 -  | less_nat n Zero_nat = false
    1.19 -  | less_nat (Suc m) (Suc n) = less_nat m n;
    1.20 +fun less_nat Zero_nat (Suc n) = true;
    1.21  
    1.22  fun less_eq_nat m n = HOL.nota (less_nat n m);
    1.23  
    1.24 @@ -25,7 +22,9 @@
    1.25  structure Codegen = 
    1.26  struct
    1.27  
    1.28 -fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
    1.29 +fun in_interval (k, l) n = (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l)
    1.30 +  | in_interval (k, l) n =
    1.31 +    (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
    1.32  
    1.33  end; (*struct Codegen*)
    1.34