--- a/src/HOL/Complete_Lattices.thy Sun Jan 29 13:58:03 2017 +0100
+++ b/src/HOL/Complete_Lattices.thy Sun Jan 29 17:27:02 2017 +0100
@@ -1320,11 +1320,7 @@
by (auto simp add: inj_on_def) blast
lemma bij_image_INT: "bij f \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
- apply (simp only: bij_def)
- apply (simp only: inj_on_def surj_def)
- apply auto
- apply blast
- done
+ by (auto simp: bij_def inj_def surj_def) blast
lemma UNION_fun_upd: "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
by (auto simp add: set_eq_iff)