# HG changeset patch
# User wenzelm
# Date 1393011433 -3600
# Node ID f0f895716a8bb4006076a0267b9bb7789b35b2b1
# Parent  4089f6e98ab91b6b4110482bd4ea24b1a9ec342e
proper ML structure with signature;

diff -r 4089f6e98ab9 -r f0f895716a8b src/HOL/Hoare/Hoare_Logic.thy
--- 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
diff -r 4089f6e98ab9 -r f0f895716a8b src/HOL/Hoare/Hoare_Logic_Abort.thy
--- 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: *)
diff -r 4089f6e98ab9 -r f0f895716a8b src/HOL/Hoare/hoare_tac.ML
--- 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;
+
diff -r 4089f6e98ab9 -r f0f895716a8b src/HOL/Isar_Examples/Hoare.thy
--- 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"