src/HOL/Set.ML
changeset 5490 85855f65d0c6
parent 5450 fe9d103464a4
child 5521 7970832271cc
     1.1 --- a/src/HOL/Set.ML	Tue Sep 15 13:09:23 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Tue Sep 15 15:04:07 1998 +0200
     1.3 @@ -295,19 +295,19 @@
     1.4  
     1.5  section "Set complement -- Compl";
     1.6  
     1.7 -qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : Compl(A)) = (c~:A)"
     1.8 +qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : -A) = (c~:A)"
     1.9   (fn _ => [ (Blast_tac 1) ]);
    1.10  
    1.11  Addsimps [Compl_iff];
    1.12  
    1.13 -val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : Compl(A)";
    1.14 +val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : -A";
    1.15  by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
    1.16  qed "ComplI";
    1.17  
    1.18  (*This form, with negated conclusion, works well with the Classical prover.
    1.19    Negated assumptions behave like formulae on the right side of the notional
    1.20    turnstile...*)
    1.21 -Goalw [Compl_def] "c : Compl(A) ==> c~:A";
    1.22 +Goalw [Compl_def] "c : -A ==> c~:A";
    1.23  by (etac CollectD 1);
    1.24  qed "ComplD";
    1.25