src/HOL/Set.ML
changeset 5931 325300576da7
parent 5649 1bac26652f45
child 6006 d2e271b8d651
     1.1 --- a/src/HOL/Set.ML	Wed Nov 18 11:12:29 1998 +0100
     1.2 +++ b/src/HOL/Set.ML	Wed Nov 18 15:10:46 1998 +0100
     1.3 @@ -299,7 +299,7 @@
     1.4  val Pow_top = subset_refl RS PowI;             (* A : Pow(A) *)
     1.5  
     1.6  
     1.7 -section "Set complement -- Compl";
     1.8 +section "Set complement";
     1.9  
    1.10  qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : -A) = (c~:A)"
    1.11   (fn _ => [ (Blast_tac 1) ]);