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