# HG changeset patch
# User wenzelm
# Date 1160353192 -7200
# Node ID c1ba49ade6a5222f747f159ed554e3c31f9cf88c
# Parent  3aa6c5bfdcbb5b1c136e3cde1127f5c54736acba
standardized facts;

diff -r 3aa6c5bfdcbb -r c1ba49ade6a5 src/HOL/Integ/IntArith.thy
--- 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]
 
diff -r 3aa6c5bfdcbb -r c1ba49ade6a5 src/HOL/Integ/Numeral.thy
--- 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]