INST : (term,term) subst -> thm -> thm
STRUCTURE
Thm
SYNOPSIS
Instantiates free variables in a theorem.
DESCRIPTION
INST is a rule for substituting arbitrary terms for free variables in a theorem. 
             A |- t               INST [x1 |-> t1,...,xn |-> tn]
   -----------------------------
    A[t1,...,tn/x1,...,xn] 
     |- 
    t[t1,...,tn/x1,...,xn]

FAILURE
Fails if, for 1 <= i <= n, some xi is not a variable, or if some xi has a different type than its intended replacement ti.
EXAMPLE
In the following example a theorem is instantiated for a specific term: 
  
   - load"arithmeticTheory";

   - CONJUNCT1 arithmeticTheory.ADD_CLAUSES;
   > val it = |- 0 + m = m : thm

   - INST [``m:num`` |-> ``2*x``] 
          (CONJUNCT1 arithmeticTheory.ADD_CLAUSES);

   val it = |- 0 + (2 * x) = 2 * x : thm

SEEALSO
INST_TY_TERM, INST_TYPE, ISPEC, ISPECL, SPEC, SPECL, SUBS, subst, SUBST, |->
HOL  Kananaskis-10