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.
Unfortunately needed patch due to incompatibility with SML -- oo is infix and hence can not appear on the left handside of patterns
authorchaieb
Tue, 12 Jun 2007 20:49:56 +0200
changeset 23345 b8139ba0c940
parent 23344 fb48c590dee1
child 23346 1517207ec8b9
Unfortunately needed patch due to incompatibility with SML -- oo is infix and hence can not appear on the left handside of patterns
src/HOL/Tools/Presburger/generated_cooper.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Presburger/generated_cooper.ML	Tue Jun 12 20:49:50 2007 +0200
+++ b/src/HOL/Tools/Presburger/generated_cooper.ML	Tue Jun 12 20:49:56 2007 +0200
@@ -1,6 +1,6 @@
 structure GeneratedCooper =
 struct
-
+nonfix oo;
 fun nat i = if i < 0 then 0 else i;
 
 val one_def0 : int = (0 + 1);
isabelle