| changeset 26303 | e4f40a0ea2e1 |
| parent 25706 | 45d090186bbe |
| child 28457 | 25669513fd4c |
--- 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 = {*