1(* ========================================================================= *)
2(* Tools for reasoning about wp and wlp.                                     *)
3(* ========================================================================= *)
4
5signature wpTools =
6sig
7
8  (* A useful tactic for case-splitting conditionals *)
9  val if_cases_tac : Abbrev.thm_tactic -> Abbrev.tactic
10
11  (* A theorem tactic for use with if_cases_tac for wlp calculation *)
12  val wlp_assume_tac : Abbrev.thm_tactic
13
14  (* The main tactics for reducing Leq pre (wlp prog post) *)
15  val pure_wlp_tac : Abbrev.tactic
16  val leq_tac      : Abbrev.tactic
17  val wlp_tac      : Abbrev.tactic
18
19end
20