1structure Abbrev :> Abbrev = 2struct 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 type thm_tactic = thm -> tactic 15 type thm_tactical = thm_tactic -> thm_tactic 16 type 'a quotation = 'a Portable.frag list 17 type ('a,'b)subst = ('a,'b) Lib.subst 18end 19