# HG changeset patch
# User wenzelm
# Date 1205775424 -3600
# Node ID e4f40a0ea2e1273bce4c778c3e2c9f3a0854f19e
# Parent  68b073052e8cf320f586455004bc83efb4484553
added Compl_Collect;

diff -r 68b073052e8c -r e4f40a0ea2e1 src/HOL/Isar_examples/Hoare.thy
--- 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 = {*