src/HOL/UNITY/Comp.thy

--- a/src/HOL/UNITY/Comp.thy	Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp.thy	Sat Feb 08 16:05:33 2003 +0100
@@ -185,7 +185,7 @@
      "[| F \<in> stable {s. P (v s) (w s)};    
          G \<in> preserves v;  G \<in> preserves w |]                
       ==> F Join G \<in> stable {s. P (v s) (w s)}"
-apply (simp)
+apply simp
 apply (subgoal_tac "G \<in> preserves (funPair v w) ")
  prefer 2 apply simp 
 apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)