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 bug for serialization for uminus on ints
authorhaftmann
Sun, 23 Jul 2006 07:21:22 +0200
changeset 20186 56207a6f4cc5
parent 20185 183f08468e19
child 20187 af47971ea304
fixed bug for serialization for uminus on ints
src/HOL/Integ/IntDef.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/IntDef.thy	Sun Jul 23 07:20:52 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Sun Jul 23 07:21:22 2006 +0200
@@ -914,7 +914,7 @@
     ml ("IntInf.* (_, _)")
     haskell (infixl 7 "*")
   "uminus :: int \<Rightarrow> int"
-    ml (target_atom "~")
+    ml (target_atom "IntInf.~")
     haskell (target_atom "negate")
   "op = :: int \<Rightarrow> int \<Rightarrow> bool"
     ml ("(op =) (_ : IntInf.int, _)")
isabelle