--- a/src/HOL/Fun.thy Mon May 25 22:52:17 2015 +0200
+++ b/src/HOL/Fun.thy Tue May 26 21:58:04 2015 +0100
@@ -478,16 +478,14 @@
lemma inj_on_image_Int:
"[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B"
-apply (simp add: inj_on_def, blast)
-done
+ by (simp add: inj_on_def, blast)
lemma inj_on_image_set_diff:
- "[| inj_on f C; A<=C; B<=C |] ==> f`(A-B) = f`A - f`B"
-apply (simp add: inj_on_def, blast)
-done
+ "[| inj_on f C; A-B \<subseteq> C; B \<subseteq> C |] ==> f`(A-B) = f`A - f`B"
+ by (simp add: inj_on_def, blast)
lemma image_Int: "inj f ==> f`(A Int B) = f`A Int f`B"
-by (simp add: inj_on_def, blast)
+ by (simp add: inj_on_def, blast)
lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B"
by (simp add: inj_on_def, blast)