src/HOL/Hoare/hoare_tac.ML
changeset 55660 f0f895716a8b
parent 55659 4089f6e98ab9
child 55661 ec14796cd140
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 20:29:33 2014 +0100
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 20:37:13 2014 +0100
     1.3 @@ -4,7 +4,14 @@
     1.4  Derivation of the proof rules and, most importantly, the VCG tactic.
     1.5  *)
     1.6  
     1.7 -(* FIXME structure Hoare: HOARE *)
     1.8 +signature HOARE =
     1.9 +sig
    1.10 +  val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool -> int -> tactic
    1.11 +  val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic
    1.12 +end;
    1.13 +
    1.14 +structure Hoare: HOARE =
    1.15 +struct
    1.16  
    1.17  (*** The tactics ***)
    1.18  
    1.19 @@ -178,3 +185,5 @@
    1.20  fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) =>
    1.21    SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
    1.22  
    1.23 +end;
    1.24 +