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