Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/List.thy
changeset 46898 1570b30ee040
parent 46884 154dc6ec0041
child 47108 2a1953f0d20d 
--- a/src/HOL/List.thy	Tue Mar 13 12:51:52 2012 +0100
+++ b/src/HOL/List.thy	Tue Mar 13 13:31:26 2012 +0100
@@ -4483,7 +4483,8 @@
   shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
 proof -
   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
-  with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
+  from assms show ?thesis
+    by (simp add: sorted_list_of_set_def fold_insert_remove)
 qed
 
 lemma sorted_list_of_set [simp]:
isabelle