1signature Abbrev =
2sig
3  type thm          = Thm.thm
4  type term         = Term.term
5  type hol_type     = Type.hol_type
6  type conv         = term -> thm
7  type rule         = thm -> thm
8  type goal         = term list * term
9  type validation   = thm list -> thm
10  type tactic       = goal -> goal list * validation
11  type list_validation = thm list -> thm list
12  type list_tactic  = goal list -> goal list * list_validation
13  type ('a,'b) gentactic = 'a -> goal list * (thm list -> 'b)
14      (* ['a |-> goal, 'b -> thm] gives tactic;
15         ['a |-> goal list, 'b -> thm list] gives list_tactic *)
16  type thm_tactic   = thm -> tactic
17  type thm_tactical = thm_tactic -> thm_tactic
18  type 'a quotation = 'a Portable.frag list
19  type ('a,'b)subst = ('a,'b) Lib.subst
20end
21