author | huffman |
Thu, 23 Feb 2012 15:04:51 +0100 | |
changeset 46607 | 6ae8121448af |
parent 46606 | 7a5c05b5f945 |
child 46608 | 37e383cc7831 |
--- a/src/HOL/Word/Bit_Representation.thy Thu Feb 23 14:43:01 2012 +0100 +++ b/src/HOL/Word/Bit_Representation.thy Thu Feb 23 15:04:51 2012 +0100 @@ -708,10 +708,6 @@ lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)" by (simp add : no_sbintr m2pths) -lemma bintrunc_Suc: - "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin" - by (case_tac bin rule: bin_exhaust) auto - lemma sign_Pls_ge_0: "(bin_sign bin = 0) = (bin >= (0 :: int))" unfolding bin_sign_def by simp