# HG changeset patch
# User haftmann
# Date 1387316066 -3600
# Node ID cdc6d8cbf7702d39336cff524cfe45fa07f226da
# Parent  e58623a33ba5a66b4b301db21bb05cec1a2ff281
avoid clashes of fact names

diff -r e58623a33ba5 -r cdc6d8cbf770 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Tue Dec 17 20:21:22 2013 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy	Tue Dec 17 22:34:26 2013 +0100
@@ -89,7 +89,7 @@
   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
   by transfer rule
 
-lemma (in ring_1) of_int_code:
+lemma (in ring_1) of_int_code_if:
   "of_int k = (if k = 0 then 0
      else if k < 0 then - of_int (- k)
      else let
@@ -99,11 +99,11 @@
 proof -
   from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   show ?thesis
-    by (simp add: Let_def divmod_int_mod_div not_mod_2_eq_0_eq_1
-      of_int_add [symmetric]) (simp add: * mult_commute)
+    by (simp add: Let_def divmod_int_mod_div of_int_add [symmetric])
+      (simp add: * mult_commute)
 qed
 
-declare of_int_code [code]
+declare of_int_code_if [code]
 
 lemma [code]:
   "nat = nat_of_integer \<circ> of_int"
diff -r e58623a33ba5 -r cdc6d8cbf770 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Tue Dec 17 20:21:22 2013 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy	Tue Dec 17 22:34:26 2013 +0100
@@ -78,7 +78,7 @@
 
 lemma [code]:
   "Divides.divmod_nat m n = (m div n, m mod n)"
-  by (simp add: prod_eq_iff)
+  by (fact divmod_nat_div_mod)
 
 lemma [code]:
   "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
@@ -96,7 +96,7 @@
   "num_of_nat = num_of_integer \<circ> of_nat"
   by transfer (simp add: fun_eq_iff)
 
-lemma (in semiring_1) of_nat_code:
+lemma (in semiring_1) of_nat_code_if:
   "of_nat n = (if n = 0 then 0
      else let
        (m, q) = divmod_nat n 2;
@@ -105,12 +105,11 @@
 proof -
   from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
   show ?thesis
-    by (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
-      of_nat_add [symmetric])
+    by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
       (simp add: * mult_commute of_nat_mult add_commute)
 qed
 
-declare of_nat_code [code]
+declare of_nat_code_if [code]
 
 definition int_of_nat :: "nat \<Rightarrow> int" where
   [code_abbrev]: "int_of_nat = of_nat"
@@ -134,13 +133,13 @@
            [typerep.Typerep (STR ''Code_Numeral.integer'') [],
          typerep.Typerep (STR ''Nat.nat'') []]))
      (term_of_class.term_of (integer_of_nat n))"
-by(simp add: term_of_anything)
+  by (simp add: term_of_anything)
 
 lemma nat_of_integer_code_post [code_post]:
   "nat_of_integer 0 = 0"
   "nat_of_integer 1 = 1"
   "nat_of_integer (numeral k) = numeral k"
-by(transfer, simp)+
+  by (transfer, simp)+
 
 code_identifier
   code_module Code_Target_Nat \<rightharpoonup>