src/HOL/UNITY/Comp.thy
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 13819 78f5885b76a9
     1.1 --- a/src/HOL/UNITY/Comp.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4       "[| F \<in> stable {s. P (v s) (w s)};    
     1.5           G \<in> preserves v;  G \<in> preserves w |]                
     1.6        ==> F Join G \<in> stable {s. P (v s) (w s)}"
     1.7 -apply (simp)
     1.8 +apply simp
     1.9  apply (subgoal_tac "G \<in> preserves (funPair v w) ")
    1.10   prefer 2 apply simp 
    1.11  apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)