added numeral code postprocessor rules on type int
authorhaftmann
Wed, 29 Jul 2009 16:42:47 +0200
changeset 32272 cc1bf9077167
parent 32269 b642e4813e53
child 32273 3c395fc7ec5e
added numeral code postprocessor rules on type int
src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Jul 29 09:06:49 2009 +0200
+++ b/src/HOL/Int.thy	Wed Jul 29 16:42:47 2009 +0200
@@ -1000,11 +1000,11 @@
   Converting numerals 0 and 1 to their abstract versions.
 *}
 
-lemma numeral_0_eq_0 [simp]:
+lemma numeral_0_eq_0 [simp, code_post]:
   "Numeral0 = (0::'a::number_ring)"
   unfolding number_of_eq numeral_simps by simp
 
-lemma numeral_1_eq_1 [simp]:
+lemma numeral_1_eq_1 [simp, code_post]:
   "Numeral1 = (1::'a::number_ring)"
   unfolding number_of_eq numeral_simps by simp