1(* ===================================================================== *) 2(* FILE : hol88Lib.sig *) 3(* DESCRIPTION : Signature for routines that provide a limited amount *) 4(* of hol88 compatibility. (To operate much as in hol88, *) 5(* one would open Psyntax and hol88Lib.) *) 6(* *) 7(* This interface is deprecated; please DO NOT USE in new code. *) 8(* ===================================================================== *) 9 10signature hol88Lib = 11sig 12 include Abbrev 13 14 type ('a,'b)hol88subst = ('b * 'a) list 15 16 val match : term -> term -> (term * term) list * (hol_type * hol_type) list 17 val assoc : ''a -> (''a * 'b) list -> ''a * 'b 18 val rev_assoc : ''a -> ('b * ''a) list -> 'b * ''a 19 val frees : term -> term list 20 val GEN_ALL : thm -> thm 21 val GEN_REWRITE_RULE : (conv -> conv) -> thm list -> thm list -> thm -> thm 22 val GEN_REWRITE_TAC : (conv -> conv) -> thm list -> thm list -> tactic 23 val variant : term list -> term -> term 24 25 (*------------------------------------------------------------------------- 26 Functions that generate and use Hol88 style substitutions. A Hol88 27 substitution is a list of pairs 28 29 [(M1,v1), ..., (Mk,vk)] 30 31 which maps to the Hol98 substitution 32 33 [{redex=v1, residue=M1}, ..., {redex=vk, residue=Mk}] 34 -------------------------------------------------------------------------*) 35 36 val match_type : hol_type -> hol_type -> (hol_type,hol_type)hol88subst 37 val subst : (term,term)hol88subst -> term -> term 38 val inst : (hol_type,hol_type)hol88subst -> term -> term 39 val match_term : term -> term 40 -> (term,term)hol88subst * (hol_type,hol_type)hol88subst 41 val SUBST : (term,thm)hol88subst -> term -> thm -> thm 42 val INST : (term,term)hol88subst -> thm -> thm 43 val INST_TYPE : (hol_type,hol_type)hol88subst -> thm -> thm 44 val INST_TY_TERM : (term,term)hol88subst * (hol_type,hol_type)hol88subst 45 -> thm -> thm 46 47end 48