# 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 \ InternalCSets ==> UNIV - X \ 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*}