simplify some proofs

--- a/src/HOLCF/ex/Hoare.thy	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOLCF/ex/Hoare.thy	Wed Nov 03 15:03:16 2010 -0700
@@ -95,9 +95,7 @@
 
 
 lemma hoare_lemma28: "f$(y::'a)=(UU::tr) ==> f$UU = UU"
-apply (erule flat_codom [THEN disjE])
-apply auto
-done
+by (rule strictI)
 
 
 (* ----- access to definitions ----- *)

--- a/src/HOLCF/ex/Loop.thy	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOLCF/ex/Loop.thy	Wed Nov 03 15:03:16 2010 -0700
@@ -47,8 +47,7 @@
 apply simp
 apply (rule allI)
 apply (rule trans)
-apply (subst while_unfold)
-apply (rule_tac [2] refl)
+apply (rule while_unfold)
 apply (subst iterate_Suc2)
 apply (rule trans)
 apply (erule_tac [2] spec)
@@ -57,9 +56,7 @@
 apply simp
 apply (subst while_unfold)
 apply (rule_tac s = "UU" and t = "b$UU" in ssubst)
-apply (erule flat_codom [THEN disjE])
-apply assumption
-apply (erule spec)
+apply (erule strictI)
 apply simp
 apply simp
 apply simp