src/HOL/Isar_examples/Hoare.thy

   done
 
 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