--- a/src/HOL/Num.thy Sun Aug 18 15:29:50 2013 +0200
+++ b/src/HOL/Num.thy Sun Aug 18 15:29:50 2013 +0200
@@ -529,6 +529,12 @@
lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"
by (rule numeral_mult [symmetric])
+lemma mult_2: "2 * z = z + z"
+ unfolding one_add_one [symmetric] distrib_right by simp
+
+lemma mult_2_right: "z * 2 = z + z"
+ unfolding one_add_one [symmetric] distrib_left by simp
+
end
subsubsection {*
@@ -544,12 +550,6 @@
by (induct n,
simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
-lemma mult_2: "2 * z = z + z"
- unfolding one_add_one [symmetric] distrib_right by simp
-
-lemma mult_2_right: "z * 2 = z + z"
- unfolding one_add_one [symmetric] distrib_left by simp
-
end
lemma nat_of_num_numeral [code_abbrev]: