--- 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
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Fri Feb 21 20:29:33 2014 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Fri Feb 21 20:37:13 2014 +0100
@@ -107,12 +107,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"
(* Special syntax for guarded statements and guarded array updates: *)
--- a/src/HOL/Hoare/hoare_tac.ML Fri Feb 21 20:29:33 2014 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Fri Feb 21 20:37:13 2014 +0100
@@ -4,7 +4,14 @@
Derivation of the proof rules and, most importantly, the VCG tactic.
*)
-(* FIXME structure Hoare: HOARE *)
+signature HOARE =
+sig
+ val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool -> int -> tactic
+ val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic
+end;
+
+structure Hoare: HOARE =
+struct
(*** The tactics ***)
@@ -178,3 +185,5 @@
fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) =>
SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
+end;
+
--- a/src/HOL/Isar_Examples/Hoare.thy Fri Feb 21 20:29:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Fri Feb 21 20:37:13 2014 +0100
@@ -400,7 +400,7 @@
method_setup hoare = {*
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD'
- (hoare_tac ctxt
+ (Hoare.hoare_tac ctxt
(simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] ))))) *}
"verification condition generator for Hoare logic"