| changeset 45604 | 29cf40fe8daf |
| parent 45543 | 827bf668c822 |
| child 45845 | 4158f35a5c6f |
--- a/src/HOL/Word/Bit_Int.thy Sun Nov 20 20:26:13 2011 +0100 +++ b/src/HOL/Word/Bit_Int.thy Sun Nov 20 20:59:30 2011 +0100 @@ -459,10 +459,10 @@ by auto lemmas bin_sc_Suc_minus = - trans [OF bin_sc_minus [symmetric] bin_sc.Suc, standard] + trans [OF bin_sc_minus [symmetric] bin_sc.Suc] lemmas bin_sc_Suc_pred [simp] = - bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard] + bin_sc_Suc_minus [of "number_of bin", simplified nobm1] for bin subsection {* Splitting and concatenation *}