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''
haftmann@21341
     1
structure ROOT = 
haftmann@21341
     2
struct
haftmann@21341
     3
haftmann@21341
     4
structure HOL = 
haftmann@21341
     5
struct
haftmann@21341
     6
haftmann@21341
     7
fun nota false = true
haftmann@21341
     8
  | nota true = false;
haftmann@21341
     9
haftmann@21341
    10
end; (*struct HOL*)
haftmann@21341
    11
haftmann@21341
    12
structure Nat = 
haftmann@21341
    13
struct
haftmann@21341
    14
haftmann@21341
    15
datatype nat = Zero_nat | Suc of nat;
haftmann@21341
    16
haftmann@21341
    17
fun less_nat Zero_nat (Suc n) = true
haftmann@21341
    18
  | less_nat n Zero_nat = false
haftmann@21341
    19
  | less_nat (Suc m) (Suc n) = less_nat m n;
haftmann@21341
    20
haftmann@21341
    21
fun less_eq_nat m n = HOL.nota (less_nat n m);
haftmann@21341
    22
haftmann@21341
    23
end; (*struct Nat*)
haftmann@21341
    24
haftmann@21341
    25
structure Codegen = 
haftmann@21341
    26
struct
haftmann@21341
    27
haftmann@21341
    28
fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
haftmann@21341
    29
haftmann@21341
    30
end; (*struct Codegen*)
haftmann@21341
    31
haftmann@21341
    32
end; (*struct ROOT*)