# HG changeset patch
# User haftmann
# Date 1376832590 -7200
# Node ID 7e3f39bc41dfad113557c81aa007d8b9f1987dac
# Parent  8f7ac535892f6c343be32a7ba1b70cc19d91b4be
generalized sort constraint of lemmas

diff -r 8f7ac535892f -r 7e3f39bc41df src/HOL/Num.thy
--- 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]: