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.
standardized facts;
authorwenzelm
Mon, 09 Oct 2006 02:19:52 +0200
changeset 20900 c1ba49ade6a5
parent 20899 3aa6c5bfdcbb
child 20901 437ca370dbd7
standardized facts;
src/HOL/Integ/IntArith.thy file | annotate | diff | comparison | revisions
src/HOL/Integ/Numeral.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/IntArith.thy	Mon Oct 09 02:19:51 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy	Mon Oct 09 02:19:52 2006 +0200
@@ -408,8 +408,7 @@
 
 lemmas int_code_rewrites =
   arith_simps(5-27)
-  arith_extra_simps(1-4) [where ?'a1 = int]
-  arith_extra_simps(5) [where ?'a = int]
+  arith_extra_simps(1-5) [where 'a = int]
 
 declare int_code_rewrites [code func]
 
--- a/src/HOL/Integ/Numeral.thy	Mon Oct 09 02:19:51 2006 +0200
+++ b/src/HOL/Integ/Numeral.thy	Mon Oct 09 02:19:52 2006 +0200
@@ -473,7 +473,7 @@
 
 subsection {* Simplification of arithmetic operations on integer constants. *}
 
-lemmas arith_extra_simps = 
+lemmas arith_extra_simps [standard] =
   number_of_add [symmetric]
   number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
   number_of_mult [symmetric]
isabelle