| 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) ]);