removed redundant line
authorpaulson
Tue May 27 11:46:29 2003 +0200 (2003-05-27)
changeset 140476123bfc55247
parent 14046 6616e6c53d48
child 14048 03a9adec9869
removed redundant line
src/HOL/UNITY/Comp.thy
     1.1 --- a/src/HOL/UNITY/Comp.thy	Tue May 27 11:39:03 2003 +0200
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Tue May 27 11:46:29 2003 +0200
     1.3 @@ -199,7 +199,6 @@
     1.4  apply (blast intro: constrains_weaken)
     1.5  (*The G case remains*)
     1.6  apply (auto simp add: preserves_def stable_def constrains_def)
     1.7 -apply (case_tac "act: Acts F", blast)
     1.8  (*We have a G-action, so delete assumptions about F-actions*)
     1.9  apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
    1.10  apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)