doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
changeset 22015 12b94d7f7e1f
parent 21994 dfa5133dbe73
child 22386 4ebe883b02ff
equal deleted inserted replaced
22014:4b70cbd96007 22015:12b94d7f7e1f
    24 
    24 
    25 structure Codegen = 
    25 structure Codegen = 
    26 struct
    26 struct
    27 
    27 
    28 fun in_interval (k, l) n =
    28 fun in_interval (k, l) n =
    29   (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
    29   Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
    30 
    30 
    31 end; (*struct Codegen*)
    31 end; (*struct Codegen*)
    32 
    32 
    33 end; (*struct ROOT*)
    33 end; (*struct ROOT*)