fix proof

--- a/src/HOL/Complex/CStar.thy	Tue Sep 06 19:28:58 2005 +0200
+++ b/src/HOL/Complex/CStar.thy	Tue Sep 06 20:53:27 2005 +0200
@@ -186,6 +186,7 @@
 
 lemma InternalCSets_UNIV_diff:
     "X \<in> InternalCSets ==> UNIV - X \<in> InternalCSets"
+apply (subgoal_tac "UNIV - X = - X")
 by (auto intro: InternalCSets_Compl)
 
 text{*Nonstandard extension of a set (defined using a constant sequence) as a special case of an internal set*}