# HG changeset patch
# User huffman
# Date 1187908632 -7200
# Node ID 737622204802e6ce7b3f60b4868e19ce51a5e8bf
# Parent  7e42e986b1a11a3086d7b60ee89365cfef884ee6
remove unused lemmas

diff -r 7e42e986b1a1 -r 737622204802 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Fri Aug 24 00:23:51 2007 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Fri Aug 24 00:37:12 2007 +0200
@@ -17,18 +17,8 @@
 
 (** ways in which type Bin resembles a datatype **)
 
-lemmas BIT_eqE = BIT_eq [THEN conjE, standard]
-
 lemmas BIT_eqI = conjI [THEN BIT_eq_iff [THEN iffD2]]
 
-lemma less_Bits: 
-  "(v BIT b < w BIT c) = (v < w | v <= w & b = bit.B0 & c = bit.B1)"
-  unfolding Bit_def by (auto split: bit.split)
-
-lemma le_Bits: 
-  "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= bit.B1 | c ~= bit.B0))" 
-  unfolding Bit_def by (auto split: bit.split)
-
 lemma neB1E [elim!]:
   assumes ne: "y \<noteq> bit.B1"
   assumes y: "y = bit.B0 \<Longrightarrow> P"
@@ -38,9 +28,6 @@
   apply (simp add: ne)
   done
 
-lemma bin_ex_rl: "EX w b. w BIT b = bin"
-  by (insert BIT_exhausts [of bin], auto)
-
 lemma bin_exhaust:
   assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
   shows "Q"
@@ -247,12 +234,6 @@
 
 text "Simplifications for (s)bintrunc"
 
-lemma bit_bool:
-  "(b = (b' = bit.B1)) = (b' = (if b then bit.B1 else bit.B0))"
-  by (cases b') auto
-
-lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
-
 lemma bin_sign_lem:
   "!!bin. (bin_sign (sbintrunc n bin) = Numeral.Min) = bin_nth bin n"
   apply (induct n)