Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Isar_examples/Hoare.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 31723 f5cafe803b55 
--- a/src/HOL/Isar_examples/Hoare.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -454,7 +454,7 @@
 use "~~/src/HOL/Hoare/hoare_tac.ML"
 
 method_setup hoare = {*
-  Method.ctxt_args (fn ctxt =>
+  Scan.succeed (fn ctxt =>
     (SIMPLE_METHOD'
        (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *}
   "verification condition generator for Hoare logic"
isabelle