# HG changeset patch
# User wenzelm
# Date 1467750197 -7200
# Node ID 6bf5a8c78175f4f23d34d525a31b0779482d9864
# Parent  a528d24826c54e2b0f247b77fdb443ff21e66049
tuned;

diff -r a528d24826c5 -r 6bf5a8c78175 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jul 05 21:23:21 2016 +0200
+++ b/src/HOL/Set.thy	Tue Jul 05 22:23:17 2016 +0200
@@ -466,7 +466,7 @@
   \<comment> \<open>Classical elimination rule.\<close>
   by (auto simp add: less_eq_set_def le_fun_def)
 
-lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)"
+lemma subset_eq: "A \<subseteq> B = (\<forall>x\<in>A. x \<in> B)"
   by blast
 
 lemma contra_subsetD: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A"
@@ -942,7 +942,7 @@
 lemma image_diff_subset: "f ` A - f ` B \<subseteq> f ` (A - B)"
   by blast
 
-lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A"
+lemma Setcompr_eq_image: "{f x |x. x \<in> A} = f ` A"
   by blast
 
 lemma setcompr_eq_image: "{f x |x. P x} = f ` {x. P x}"
@@ -978,10 +978,8 @@
 lemma range_composition: "range (\<lambda>x. f (g x)) = f ` range g"
   by auto
 
-lemma range_eq_singletonD:
-  assumes "range f = {a}"
-  shows "f x = a"
-  using assms by auto
+lemma range_eq_singletonD: "range f = {a} \<Longrightarrow> f x = a"
+  by auto
 
 
 subsubsection \<open>Some rules with \<open>if\<close>\<close>