--- a/src/HOL/Hoare/Hoare_Logic.thy Fri Feb 21 20:29:33 2014 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy Fri Feb 21 20:37:13 2014 +0100
@@ -96,12 +96,12 @@
ML_file "hoare_tac.ML"
method_setup vcg = {*
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac))) *}
"verification condition generator"
method_setup vcg_simp = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac ctxt))) *}
+ SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt))) *}
"verification condition generator plus simplification"
end