fixed bug for serialization for uminus on ints
authorhaftmann
Sun Jul 23 07:21:22 2006 +0200 (2006-07-23)
changeset 2018656207a6f4cc5
parent 20185 183f08468e19
child 20187 af47971ea304
fixed bug for serialization for uminus on ints
src/HOL/Integ/IntDef.thy
     1.1 --- a/src/HOL/Integ/IntDef.thy	Sun Jul 23 07:20:52 2006 +0200
     1.2 +++ b/src/HOL/Integ/IntDef.thy	Sun Jul 23 07:21:22 2006 +0200
     1.3 @@ -914,7 +914,7 @@
     1.4      ml ("IntInf.* (_, _)")
     1.5      haskell (infixl 7 "*")
     1.6    "uminus :: int \<Rightarrow> int"
     1.7 -    ml (target_atom "~")
     1.8 +    ml (target_atom "IntInf.~")
     1.9      haskell (target_atom "negate")
    1.10    "op = :: int \<Rightarrow> int \<Rightarrow> bool"
    1.11      ml ("(op =) (_ : IntInf.int, _)")