src/HOL/List.thy
changeset 46898 1570b30ee040
parent 46884 154dc6ec0041
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/List.thy	Tue Mar 13 12:51:52 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Mar 13 13:31:26 2012 +0100
     1.3 @@ -4483,7 +4483,8 @@
     1.4    shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
     1.5  proof -
     1.6    interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
     1.7 -  with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
     1.8 +  from assms show ?thesis
     1.9 +    by (simp add: sorted_list_of_set_def fold_insert_remove)
    1.10  qed
    1.11  
    1.12  lemma sorted_list_of_set [simp]: