--- a/src/HOL/Library/Code_Target_Int.thy Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy Wed Feb 13 13:38:52 2013 +0100
@@ -26,18 +26,18 @@
by (simp add: integer_of_num_def fun_eq_iff)
lemma [code_abbrev]:
- "int_of_integer (Code_Numeral_Types.Pos k) = Int.Pos k"
+ "int_of_integer (numeral k) = Int.Pos k"
by simp
lemma [code_abbrev]:
- "int_of_integer (Code_Numeral_Types.Neg k) = Int.Neg k"
+ "int_of_integer (neg_numeral k) = Int.Neg k"
by simp
-
-lemma [code]:
+
+lemma [code, symmetric, code_post]:
"0 = int_of_integer 0"
by simp
-lemma [code]:
+lemma [code, symmetric, code_post]:
"1 = int_of_integer 1"
by simp