added Compl_Collect;

--- a/src/HOL/Isar_examples/Hoare.thy	Mon Mar 17 18:37:03 2008 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Mon Mar 17 18:37:04 2008 +0100
@@ -446,6 +446,9 @@
   apply blast
   done
 
+lemma Compl_Collect: "- Collect b = {x. \<not> b x}"
+  by blast
+
 use "~~/src/HOL/Hoare/hoare_tac.ML"
 
 method_setup hoare = {*