# HG changeset patch
# User paulson
# Date 1054028789 -7200
# Node ID 6123bfc552472955568824c1a5729d5b0694dfc8
# Parent  6616e6c53d48de157e0a2653bce00296f585bb1c
removed redundant line

diff -r 6616e6c53d48 -r 6123bfc55247 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Tue May 27 11:39:03 2003 +0200
+++ b/src/HOL/UNITY/Comp.thy	Tue May 27 11:46:29 2003 +0200
@@ -199,7 +199,6 @@
 apply (blast intro: constrains_weaken)
 (*The G case remains*)
 apply (auto simp add: preserves_def stable_def constrains_def)
-apply (case_tac "act: Acts F", blast)
 (*We have a G-action, so delete assumptions about F-actions*)
 apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
 apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)