| changeset 63793 | e68a0b651eb5 |
| parent 61343 | 5b5656a63bd6 |
| child 66110 | d59f9f696110 |
--- a/src/HOL/ex/Bubblesort.thy Mon Sep 05 15:00:37 2016 +0200 +++ b/src/HOL/ex/Bubblesort.thy Mon Sep 05 15:47:50 2016 +0200 @@ -58,7 +58,6 @@ apply simp apply simp by(auto split: list.splits if_splits dest: bubble_minD_mset) - (metis add_eq_conv_ex mset_bubble_min mset.simps(2)) lemma set_bubblesort: "set (bubblesort xs) = set xs" by(rule mset_bubblesort[THEN mset_eq_setD])