# HG changeset patch
# User huffman
# Date 1288821796 25200
# Node ID 5f37c39648665152554583c6382c72182d18c53f
# Parent  3b7f570723f9908e5b29662b04c508359817bd66
simplify some proofs

diff -r 3b7f570723f9 -r 5f37c3964866 src/HOLCF/ex/Hoare.thy
--- 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 ----- *)
diff -r 3b7f570723f9 -r 5f37c3964866 src/HOLCF/ex/Loop.thy
--- 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