doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
author haftmann
Mon Nov 13 15:55:38 2006 +0100 (2006-11-13)
changeset 21341 3844037a8e2d
child 21993 4b802a9e0738
permissions -rw-r--r--
adjusted to new fun''
     1 structure ROOT = 
     2 struct
     3 
     4 structure HOL = 
     5 struct
     6 
     7 fun nota false = true
     8   | nota true = false;
     9 
    10 end; (*struct HOL*)
    11 
    12 structure Nat = 
    13 struct
    14 
    15 datatype nat = Zero_nat | Suc of nat;
    16 
    17 fun less_nat Zero_nat (Suc n) = true
    18   | less_nat n Zero_nat = false
    19   | less_nat (Suc m) (Suc n) = less_nat m n;
    20 
    21 fun less_eq_nat m n = HOL.nota (less_nat n m);
    22 
    23 end; (*struct Nat*)
    24 
    25 structure Codegen = 
    26 struct
    27 
    28 fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
    29 
    30 end; (*struct Codegen*)
    31 
    32 end; (*struct ROOT*)