File: ISPECL.doc

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (28 lines) | stat: -rw-r--r-- 674 bytes parent folder | download | duplicates (11) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
 
\DOC ISPECL

\TYPE {ISPECL : (term list -> thm -> thm)}

\SYNOPSIS
Specializes a theorem zero or more times, with type instantiation if necessary.

\KEYWORDS
rule, type.

\DESCRIBE
{ISPECL} is an iterative version of {ISPEC}
{
         A |- !x1...xn.t
   ----------------------------  ISPECL ["t1",...,"tn"]
    A |- t[t1,...tn/x1,...,xn]
}
\noindent (where {ti} is free for {xi} in {tm}).

\FAILURE
{ISPECL} fails if the list of terms is longer than the number of
quantified variables in the term, if the type instantiation fails, or
if the type variable being instantiated is free in the assumptions.

\SEEALSO
INST_TYPE, INST_TY_TERM, ISPEC, MATCH, SPEC, SPECL.

\ENDDOC