changeset 42809 | 5b45125b15ba |
parent 42714 | fcba668b0839 |
child 42871 | 1c0b99f950d9 |
--- a/src/HOL/List.thy Sat May 14 00:32:16 2011 +0200 +++ b/src/HOL/List.thy Sat May 14 18:26:25 2011 +0200 @@ -3765,7 +3765,7 @@ lemma fun_left_comm_insort: "fun_left_comm insort" proof -qed (fact insort_left_comm) +qed (simp add: insort_left_comm fun_eq_iff) lemma sort_key_simps [simp]: "sort_key f [] = []"