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