| changeset 20900 | c1ba49ade6a5 |
| parent 20699 | 0cc77abb185a |
| child 21046 | fe1db2f991a7 |
--- 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]