Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorLars Hupel <lars.hupel@mytum.de>
Fri, 17 Apr 2015 09:56:12 +0200
changeset 60105 8614f8f0fb4b
parent 60104 243cee7c1e19 (diff)
parent 60103 d6b043ad7b3d (current diff)
child 60106 e0d1d9203275
child 60109 22389d4cdd6b
child 60112 3eab4acaa035
merged
--- a/src/HOL/Word/Word_Miscellaneous.thy	Thu Apr 16 23:16:22 2015 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Fri Apr 17 09:56: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
isabelle