doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML
changeset 21994 dfa5133dbe73
parent 21993 4b802a9e0738
child 22386 4ebe883b02ff
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jan 04 17:11:09 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jan 04 17:17:48 2007 +0100
     1.3 @@ -4,7 +4,8 @@
     1.4  structure HOL = 
     1.5  struct
     1.6  
     1.7 -fun nota false = true;
     1.8 +fun nota false = true
     1.9 +  | nota true = false;
    1.10  
    1.11  end; (*struct HOL*)
    1.12  
    1.13 @@ -13,7 +14,9 @@
    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 +fun less_nat Zero_nat (Suc n) = true
    1.19 +  | less_nat n Zero_nat = false
    1.20 +  | less_nat (Suc m) (Suc n) = less_nat m n;
    1.21  
    1.22  fun less_eq_nat m n = HOL.nota (less_nat n m);
    1.23  
    1.24 @@ -23,9 +26,7 @@
    1.25  struct
    1.26  
    1.27  fun in_interval (k, l) n =
    1.28 -  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l)
    1.29 -  | in_interval (k, l) n =
    1.30 -    (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
    1.31 +  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
    1.32  
    1.33  end; (*struct Codegen*)
    1.34