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.
remove redundant lemmas
authorhuffman
Tue, 13 Dec 2011 11:48:59 +0100
changeset 45844 6374cd925b18
parent 45843 c58ce659ce2a
child 45845 4158f35a5c6f
remove redundant lemmas
src/HOL/Word/Bit_Representation.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 11:26:10 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 11:48:59 2011 +0100
@@ -54,12 +54,6 @@
 
 lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
 
-lemma Min_ne_Pls [iff]:  
-  "Int.Min ~= Int.Pls"
-  unfolding Min_def Pls_def by auto
-
-lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]
-
 lemmas PlsMin_defs [intro!] = 
   Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]
isabelle