src/HOL/Algebra/Lattice.thy

 	assume z: "z \<in> {a, x}"
 	then show "z \<sqsubseteq> y"
 	proof
           have y': "y \<in> Upper L A"
             apply (rule subsetD [where A = "Upper L (insert x A)"])
-            apply (rule Upper_antimono) apply clarify apply assumption
+             apply (rule Upper_antimono)
+	     apply blast
+	    apply (rule y)
             done
           assume "z = a"
           with y' least_a show ?thesis by (fast dest: least_le)
 	next
 	  assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)

           assume z: "z \<in> {a, x}"
           then show "z \<sqsubseteq> y"
           proof
             have y': "y \<in> Upper L A"
 	      apply (rule subsetD [where A = "Upper L (insert x A)"])
-	      apply (rule Upper_antimono) apply clarify apply assumption
+	      apply (rule Upper_antimono)
+	       apply blast
+	      apply (rule y)
 	      done
             assume "z = a"
             with y' least_a show ?thesis by (fast dest: least_le)
 	  next
             assume "z \<in> {x}"

 	assume z: "z \<in> {a, x}"
 	then show "y \<sqsubseteq> z"
 	proof
           have y': "y \<in> Lower L A"
             apply (rule subsetD [where A = "Lower L (insert x A)"])
-            apply (rule Lower_antimono) apply clarify apply assumption
+            apply (rule Lower_antimono)
+	     apply blast
+	    apply (rule y)
             done
           assume "z = a"
           with y' greatest_a show ?thesis by (fast dest: greatest_le)
 	next
           assume "z \<in> {x}"

           assume z: "z \<in> {a, x}"
           then show "y \<sqsubseteq> z"
           proof
             have y': "y \<in> Lower L A"
 	      apply (rule subsetD [where A = "Lower L (insert x A)"])
-	      apply (rule Lower_antimono) apply clarify apply assumption
+	      apply (rule Lower_antimono)
+	       apply blast
+	      apply (rule y)
 	      done
             assume "z = a"
             with y' greatest_a show ?thesis by (fast dest: greatest_le)
 	  next
             assume "z \<in> {x}"

           by (rule_tac greatest_LowerI) auto
       }
       ultimately show ?thesis by blast
     qed
   qed
-qed (assumption | rule total_order_axioms.intro)+
+qed (rule total total_order_axioms.intro)+
 
 
 subsection {* Complete lattices *}
 
 locale complete_lattice = lattice +

     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "complete_lattice L"
 proof intro_locales
   show "lattice_axioms L"
     by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
-qed (assumption | rule complete_lattice_axioms.intro)+
+qed (rule complete_lattice_axioms.intro sup_exists inf_exists | assumption)+
 
 constdefs (structure L)
   top :: "_ => 'a" ("\<top>\<index>")
   "\<top> == sup L (carrier L)"