# HG changeset patch
# User huffman
# Date 1126032807 -7200
# Node ID 5c613b64bf0a946058088aa583d00ab74ba2f288
# Parent  94f6113fe9ed2bddf317f29ac9e55896115ba803
fix proof

diff -r 94f6113fe9ed -r 5c613b64bf0a src/HOL/Complex/CStar.thy
--- 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*}