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/Num.thy
changeset 64238 b60a9752b6d0
parent 64178 12e6c3bbb488
child 66283 adf3155c57e2 
--- a/src/HOL/Num.thy	Sat Oct 15 23:07:47 2016 +0200
+++ b/src/HOL/Num.thy	Sun Oct 16 09:31:03 2016 +0200
@@ -1217,7 +1217,7 @@
   K (
     Lin_Arith.add_simps
       @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
-        arith_special numeral_One of_nat_simps}
+        arith_special numeral_One of_nat_simps uminus_numeral_One}
     #> Lin_Arith.add_simps
       @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
         le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc
isabelle