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 typo
authorhaftmann
Thu, 10 May 2007 22:11:35 +0200
changeset 22927 0b53bd36258b
parent 22926 fb6917e426da
child 22928 1feef3b54ce1
fixed typo
src/HOL/arith_data.ML file | annotate | diff | comparison | revisions 
--- 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