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