1(* ========================================================================= *)
2(* Version of the MESON procedure a la PTTP. Various search options.         *)
3(* ========================================================================= *)
4
5
6signature mesonLib =
7sig
8type thm = Thm.thm
9type tactic = Abbrev.tactic
10
11   val depth     : bool ref
12   val prefine   : bool ref
13   val precheck  : bool ref
14   val dcutin    : int ref
15   val skew      : int ref
16   val cache     : bool ref
17   val chatting  : int ref
18   val max_depth : int ref
19
20   val GEN_MESON_TAC : int -> int -> int -> thm list -> tactic
21   val MESON_TAC     : thm list -> tactic
22   val ASM_MESON_TAC : thm list -> tactic
23
24end (* sig *)
25