Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed type annotation
authorhaftmann
Thu, 15 Sep 2005 08:16:22 +0200
changeset 17401 9147c880ada6
parent 17400 6ede71a506f5
child 17402 41f1249bce37
fixed type annotation
src/HOL/Integ/reflected_presburger.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/reflected_presburger.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/reflected_presburger.ML	Thu Sep 15 07:35:38 2005 +0200
+++ b/src/HOL/Integ/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
 
--- 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
isabelle