doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
changeset 21341 3844037a8e2d
child 21993 4b802a9e0738
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Mon Nov 13 15:55:38 2006 +0100
     1.3 @@ -0,0 +1,32 @@
     1.4 +structure ROOT = 
     1.5 +struct
     1.6 +
     1.7 +structure HOL = 
     1.8 +struct
     1.9 +
    1.10 +fun nota false = true
    1.11 +  | nota true = false;
    1.12 +
    1.13 +end; (*struct HOL*)
    1.14 +
    1.15 +structure Nat = 
    1.16 +struct
    1.17 +
    1.18 +datatype nat = Zero_nat | Suc of nat;
    1.19 +
    1.20 +fun less_nat Zero_nat (Suc n) = true
    1.21 +  | less_nat n Zero_nat = false
    1.22 +  | less_nat (Suc m) (Suc n) = less_nat m n;
    1.23 +
    1.24 +fun less_eq_nat m n = HOL.nota (less_nat n m);
    1.25 +
    1.26 +end; (*struct Nat*)
    1.27 +
    1.28 +structure Codegen = 
    1.29 +struct
    1.30 +
    1.31 +fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
    1.32 +
    1.33 +end; (*struct Codegen*)
    1.34 +
    1.35 +end; (*struct ROOT*)