changeset 17401 | 9147c880ada6 |
parent 17390 | df2b53a66937 |
child 17426 | acfc05e02e5b |
--- a/src/HOL/Tools/Presburger/reflected_presburger.ML Thu Sep 15 07:35:38 2005 +0200 +++ b/src/HOL/Tools/Presburger/reflected_presburger.ML Thu Sep 15 08:16:22 2005 +0200 @@ -2,7 +2,7 @@ (* Caution: This file should not be modified. *) (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *) -fun (nat: IntInf.int -> IntInf.int) i = if i < 0 then 0 else i; +fun nat (i:IntInf.int) = if i < 0 then 0 else i : IntInf.int; structure Generated = struct