changeset 54863 | 82acc20ded73 |
parent 54854 | 3324a0078636 |
child 54869 | 0046711700c8 |
--- a/src/HOL/Word/Bool_List_Representation.thy Wed Dec 25 17:39:06 2013 +0100 +++ b/src/HOL/Word/Bool_List_Representation.thy Wed Dec 25 17:39:06 2013 +0100 @@ -906,7 +906,7 @@ apply (drule meta_spec) apply (erule trans) apply (drule_tac x = "bin_cat y n a" in meta_spec) - apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2) + apply (simp add : bin_cat_assoc_sym min.absorb2) done lemma bin_rcat_bl: