author | huffman |
Thu, 23 Feb 2012 11:20:42 +0100 | |
changeset 46598 | fd0ac848140e |
parent 46597 | 7fc239ebece2 |
child 46599 | 102a06189a6c |
--- a/src/HOL/Word/Bit_Representation.thy Thu Feb 23 08:59:55 2012 +0100 +++ b/src/HOL/Word/Bit_Representation.thy Thu Feb 23 11:20:42 2012 +0100 @@ -166,7 +166,7 @@ lemma bin_abs_lem: "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls --> nat (abs w) < nat (abs bin)" - apply (clarsimp simp add: bin_rl_char) + apply clarsimp apply (unfold Pls_def Min_def Bit_def) apply (cases b) apply (clarsimp, arith)