removed trivial lemmas
authorLars Hupel <lars.hupel@mytum.de>
Thu, 16 Apr 2015 17:52:12 +0200
changeset 60104 243cee7c1e19
parent 60088 0a064330a885
child 60105 8614f8f0fb4b
removed trivial lemmas
src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Thu Apr 16 15:55:55 2015 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Thu Apr 16 17:52:12 2015 +0200
@@ -154,8 +154,6 @@
 lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))" by arith
 
 lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1]
-lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified]
-lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified]
 
 lemma z1pdiv2:
   "(2 * b + 1) div 2 = (b::int)" by arith