# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1429199532 -7200
# Node ID 243cee7c1e19bd431f88d4572fd780dee4aaeeb5
# Parent  0a064330a885b8681884b14460fa2e1a3749da1f
removed trivial lemmas

diff -r 0a064330a885 -r 243cee7c1e19 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