Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/arith_data.ML
changeset 22927 0b53bd36258b
parent 22900 f8a7c10e1bd0
child 22947 f53486e661a7 
--- a/src/HOL/arith_data.ML	Thu May 10 18:10:32 2007 +0200
+++ b/src/HOL/arith_data.ML	Thu May 10 22:11:35 2007 +0200
@@ -744,7 +744,7 @@
         val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
         val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
                                         (number_of $
-                                          (Const ("Numeral.uminus",
+                                          (Const ("HOL.uminus",
                                             HOLogic.intT --> HOLogic.intT) $ k'))
         val zero_leq_j              = Const ("Orderings.less_eq",
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
isabelle