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