next up previous contents
Next: References Up: The Nuprl Proof Development Previous: The Lisp Debugger

Index

A B C D E F G H J K L M N O P Q R S T U V W X Y Z

, gif

#
$ sign
SPACE
RETURN
LINEFEED
DELETE
BACKSPACE
MOUSE-LEFT
MOUSE-MIDDLE
MOUSE-RIGHT
MOUSE-LEFT
*
-
.prl file-name extensions
.tex
.xinitrc
-wf
{ i} ( pushm)
{ } ( popm)



null
C- X
M- X
CM- X
S- X
C-C C-C
C-Z
S- RETURN
M-< CM-K CM-I
C- RETURN
abstraction
[ ]
_index
abort
AbRedexC
abstract
abstract-syntax-trees
abstract data types
abstraction , gif , gif
abstraction-meta-variables
abstraction object
abstract redices
active second-order
add_AbReduce_conv
add_soft_abs
add_theory_delimiters
AddHiddenLabel
AddHiddenLabelAndNumber
adding set definitions
AddProperties i
addr
AddXM
ADT's
alias , gif
all
alpha-conversion
alphanumeric string
alternative display
ambiguity
antecedent
ApFunToHypEquands
arguements of v
arithmetic

lemma
literal
property lemma , gif
type

arity , gif
ASCII
atom conversions

Rev*

atomic conversions
Atomic Direct-Computation Conversions
Attributed Abstractions
AUnfoldsTopC
Auto
Auto'
automatic instantiation
automatic parenthesization
autorepeat
autotactics
autotactics

Contradiction
Eq
NthDecl
NthHyp
trivial

aux
backchain
bind
binding variables
Bledsoe
break zone
break zone

hard
linear
soft

BY
Cache Dependencies
caches
capture
cases
chaining

Backchain
BackThruHyp i
BackThruLemma
backward
BHyp
BLemma
CompleteBackchain , gif
FHyp
FLemma
forward
FwdThruHyp i
FwdThruLemma
HypBackchain
InstConcl [t1;...;tn] i
InstHyp [t1;...;tn] i
InstLemma name [t1;...;tn]
optional arguments
Using [`n`.'3']

check
check-objects
classical reasoning , gif
classical tableau
clauses , gif
closure
command history
comment
Common Lisp , gif
complete
Composite Direct Computation Conversions
compressed format
computational content
conclusion
condition
conditional rewriting
conjecture , gif
consequent
constructive reasoning
context dependent notation
continuation line
continuation prompt
control
control indentation
control meta
conversion
conversion

apply_conv
RewriteType
RW
RWAddr
RWD
RWH
RWN
RWT
RWU

conversionals , gif
conversionals

AbRedexC
ANDTHENC
FirstC
ForceRedexC
HigherC
NthC
ORELSEC
RepeatC
RuleC
SUbC
SweepDnC
SweepUpC
SweepUpC : convn convn
TryC

conversion descriptions
convn
copy
Cornell Synthesizer-Generator
correct library
correctness
create_rule
create_thm
cursor
cursor

hidden
screen
screen cursor
screen mode
term
term mode
text
text mode

cursors
Cut and Paste Commands
Cutting and Pasting

copy-as-kill
items
save

CVS version control
Debugger
decidability
decide
decimal code
decision procedures
declare variables
Declaring Relations
decomposition
default abstraction
definition
definitionally equal
definitions

typed non-recursive
untyped

delete
delete_objects
delete_theory
delimiters , gif
dependency checking
destructively modified and checked
destructive modification
direct computation rules
directed graph
directory structure
display , gif
display

forms
form tree

display-meta-variables
display form , gif
display form

definition
ojbect

dummy theories
dump_theory
dumped representation
EDIT , gif
edit mode
editor

proof
term

emacs
empty string
env
env.ml
environment , gif
environment

local

eq
EqCD , gif
EqHD i
EqTypeCD
EqTypeHD
EqTypeHD i
equality-in-a-type
error messages , gif , gif
exception
exit
EXIT-TOP-LOOP
expansion
exploded
expression increments
extraction
extract term , gif
file
filled
first-order

matching

Fold a c
FontTest
force
Forester
free occurrences
garbage-collecting
GenConcl
general universal formulae
get_type
goal
goal labels
graph
grep
guard abstraction
hard zone
hidden
Hidden Hypotheses
hidden hypothesis
hidden labels
hints
HOL
horn clauses
hyp-index term
hyp-item
hyp-list hyp-item
hypothesis
HypSubst
i.P
id_ml
id_ml_inc
ID c
iff relation
immediate subgoals
immediate subterm
implicit coercions
implicitly quantified
Inclusion I
incomplete terms
indentation
index universe
inferring types
init file
initialization procedure
INITIALIZE
initialize_rw_lemma_caches : unit unit
injecting
input
insert
insertion commands
instance term
instantiated
interupt
introduction and elimination rules
intuitionistically decompose
intuitionistic propositional logic
invisible variables
invoke
Isabelle
iterated decomposition
iteration attributes
iteration families
just
justifications
justifications

comutational
tactic

kill in emacs
kind
kind

A
C
D
L
M
R
T

L'
label related tactics
layout algorithm
LCF
left to right
lemma

functionality
functionality

congruence
monotonicity
opid_functionality

inversion
inversion

opid-of-r_inversion

support
transitivity
transitivity

opid-of-transitivity_index

weakening
weakening

opid-of-weakening_index

Lemma and Hypothesis Conversions
Lemma and Hypothesis Conversions

HypC i
left-to-right
LemmaC name
Rev
right-to-left

lemmas
lemmas

antisymmetry
complementing
irreflexivity
opid-of-<_complement
opid-of-<_irreflexivity
opid-of-_antisymmetry

level-expression , gif
level-expression variables
level expression , gif , gif
level expression

syntax of

lhs
Library ML Functions
Library Window Motion
Library Window Motion

bottom
down
jump
top
up

line-breaking formats
linear zone
linebreaking
linebreaks
Lisp debugger
list-theories
load_fully_theory
load_theories_with_ancestors
load_theory
local hypotheses
logic abstractions
logical database
logical structure of terms
long_print_theory
Long Name
M-shaped graphs
MacroC
main
main goal
maintain names of binding variables
margin control format
mark
matches P
match handles
matching-constraint
Mathematica
MemCD
MemHD i
MemTypeCD
MemTypeHD i
meta
meta-bound-variables
meta-parameters , gif , gif
meta-terms
meta-variable , gif
ml
ML

abbreviations
abbreviations

(T ...) , gif

evaluating an expression
files
function

create_module

language
lists
prompt
prompt terms
strings
type level-exp
type tok
type var
view

ml-cmd
ML-HISTORY
ml object
modified keys
module types
Mouse Commands
move , gif
move-objects
myid
name , gif
Names of variables
newline terms
new term entry
non-printing characters
non-standard characters
normalizing
normal parameter
NP complete
null variable
numerals
Nuprl

book
font files
font path
fonts

nuprl-8x13
nuprl-13
nuprl-20

ML manual , gif , gif
ML Top Loop

uses

package
state
version 4.1
window

nuprlbugs
object-language
object dependencies
objects
obname
operator
opid
opid-of-_complement
opid_df
opid_properties
opid _wf , gif
optional arguments
order of strength
output
overloading
parameter
parameter

level expression
natural
string
token
variable

parameter types
parens
parenthesization , gif
parseable syntax in ASCII
parsers
passive second-order variables
paste
pattern
pattern term
permutation relation
place
place-holder
point , gif
polynomials in canonical form
positive definite formulae
precedence , gif
precedence order
prefix decidable
preprocessed lemmas
pretty-printing routines
primitive
primitive refinement rules
prl-term
proof

closed
complete
compressed
compressed format
expanded
good
incomplete
reconstruct

proof annotations
proof editor , gif
proof node display
proofs
proper subtype
property lemmas
propositions
propositions-as-types
propositions-as-types encoding
ProveDecidable
proved truth
ProvePropertiesLemma
ProveSqStable
ps-term
psterm-anno
quit , gif
rank function
re-initialize
read-only
read-only mode
recdef , gif
record types
reducible attribute
referenced automatically
refinement
refiner
region
relation

equivalence

relation families
relations , gif
relations
equivalence

computational equality relation
if and only if
mod
permutation
primitive equality relation
rationals

relfam
reln
RemoveLabel
rename
reset
reset_caches
RevHypSubst
rewrite
rewrite rules
rewriting , gif
rhs , gif
right-hand-side term
right to left
ring axioms
rnam
root goal
rule , gif
rule arg
rule objects
rule terms
RunPSTerm
RWW (ctl-str : string) i
S-expressions
save
scroll
search
second-order
second-order

binding
bindings
instance
matching , gif
substitution , gif
term
terms
variable

second-order variable instance
sequences of terms
sequent
sequent calculus
sequent clauses
set_theory_ancestors
set_theory_filename
setdef
short_print_theory
Short Name
Shostak
SHOW , gif
show_theory_filename
SIAuto
simple universal formulae
slot formats
so_apply
so_apply(n)
so_lambda
soft abstractions
soft zone
spaces
SqStable(P)
squashed exists
squash P
Squash Stability
squash stable
starting up
state
status , gif
status

#
*
-
?
bad
complete
incomplete
raw

strength of a redex
stronger-rnam
structured editors
subgoals
subrange
Subst
SubstClause
substitution
substitution

first order
term

suffix *
summary
SupInf
SupInf'
system-language
Tacs
tactic
tactic

arguments
Arith
basic tacticals

Complete T
ORELSE T2
Progress T
Repeat T
RepeatFor i T
THEN
THENL
Try T

BoolCases i
BoolCasesOnCExp
case splits
CompNatInd i
control string
Folds as c
force argument
induction
IntInd i
justification
ListInd i
NatInd i
NSubsetInd i
PRoveProp
ProveProp1
ProvePropWith (T : tactic)
Ranknd
Reduce c
RelRST
RepUnfolds as c
rewriting
rule
SplitOnConclITE
structural

AssertAt j t
Assert t
Fail
Id
MoveDepHypsToConcl j
MoveToConcl j
MoveToHyp j i
NthDecl i
NthHyp i
RenameBVars
RenameVar v i
Thin i

tacticals
tacticals

All (T : int tactic)
AllHyps
IfLabl
infix
label sensitive tacticals
multiple clause tacticals
On [c1;...;cn]
RepeatM
RepeatMFor i T
SeqOnM
THENA
THENLL
THENM
THENW

transformation
transformation

Copy
Mark
PrintTexFile
Restore
Z

Unfolds as c

tactic_rule
tactic arguments
tactic arguments

analogy tactics
analogy tactics

At (U:term) T
New ([v1;...;vn]
Sel (n:int) T
Using (sub:(var # term) list) T
With (t:term) T
WithArgs (args: (tok # arg) list) T

tactic rule
TacticText
tdef
term data-structure
term editor , gif
termination characters
term sequence
term slots , gif
terms with holes
Text Insertion

insert-spec-char-num

text sequence
text slot
text slots
text string
theorem
theorem

extraction
proof-script

theories , gif
theories

dumping
loading
theory

dependencies
dependencies of
directories
dumped to a file
of divisibility

theory-init.ml
theory-name.prl
theory-name_begin
theory-name_end
theory-name_long.prl
theory_ancestors
theory_filenames
timestamped
top-down
top loop commands
transformation tactics
transform command
transparent
tree addresses
tree walking commands
trivial conversions
trivial monotonicity
type

antecedents
declaration , gif
inclusion

underneath
Unfold a c
unfolded
unfolded soft abstractions
unfolds
Unhide
UnhideAllHypsSinceSqStableConcl
UnhideLabel
UnhideSqStableHyp i
uninstantiated
universal formulae
universal quantification
universes
unrefined leaves
variable instances are simulated
variables
variable{v}
view , gif
view function
visibility of the variable
visual presentation
well-formedness lemma
well-formedness theorems
whitespace
whitespace formatting
width
window

active
library , gif , gif
multiple
Nuprl , gif
proof
proof editor
refinement rule
rulebox
shell
term editor , gif , gif
X
wrapper

see wrapped

xmiddle abstraction
yank-next in emacs
yank in emacs
Y combinator , gif
zero width



Karla Consroe
Wed Oct 23 13:48:45 EDT 1996