--- a/src/HOL/Isar_examples/Hoare.thy Thu Oct 02 13:07:33 2008 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy Thu Oct 02 14:22:36 2008 +0200
@@ -449,12 +449,14 @@
lemma Compl_Collect: "- Collect b = {x. \<not> b x}"
by blast
+lemmas AbortRule = SkipRule -- "dummy version"
+
use "~~/src/HOL/Hoare/hoare_tac.ML"
method_setup hoare = {*
- Method.no_args
+ Method.ctxt_args (fn ctxt =>
(Method.SIMPLE_METHOD'
- (hoare_tac (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] )))) *}
+ (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *}
"verification condition generator for Hoare logic"
end