changeset 32439 | 7a91c7bcfe7e |
parent 31790 | 05c92381363c |
child 32642 | 026e7c6a6d08 |
--- a/src/HOL/Word/BinBoolList.thy Fri Aug 28 19:35:49 2009 +0200 +++ b/src/HOL/Word/BinBoolList.thy Fri Aug 28 19:43:19 2009 +0200 @@ -918,8 +918,8 @@ apply (frule asm_rl) apply (drule spec) apply (erule trans) - apply (drule_tac x = "bin_cat y n a" in spec) - apply (simp add : bin_cat_assoc_sym min_def) + apply (drule_tac x = "bin_cat y n a" in spec) + apply (simp add : bin_cat_assoc_sym) done lemma bin_rcat_bl: