Index

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

,

#

$ 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 , ,

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 ,

all

alpha-conversion

alphanumeric string

alternative display

ambiguity

antecedent

ApFunToHypEquands

arguements of v

arithmetic

lemma

literal

property lemma ,

type

arity ,

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 ,

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 ,

classical tableau

clauses ,

closure

command history

comment

Common Lisp ,

complete

Composite Direct Computation Conversions

compressed format

computational content

conclusion

condition

conditional rewriting

conjecture ,

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 ,

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 ,

dependency checking

destructively modified and checked

destructive modification

direct computation rules

directed graph

directory structure

display ,

display

forms

form tree

display-meta-variables

display form ,

display form

definition

ojbect

dummy theories

dump_theory

dumped representation

EDIT ,

edit mode

editor

proof

term

emacs

empty string

env

env.ml

environment ,

environment

local

eq

EqCD ,

EqHD i

EqTypeCD

EqTypeHD

EqTypeHD i

equality-in-a-type

error messages , ,

exception

exit

EXIT-TOP-LOOP

expansion

exploded

expression increments

extraction

extract term ,

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 ,

level-expression variables

level expression , ,

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 , ,

meta-terms

meta-variable ,

ml

ML

abbreviations

abbreviations

(T ...) ,

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 ,

move-objects

myid

name ,

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 , ,

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 ,

optional arguments

order of strength

output

overloading

parameter

parameter

level expression

natural

string

token

variable

parameter types

parens

parenthesization ,

parseable syntax in ASCII

parsers

passive second-order variables

paste

pattern

pattern term

permutation relation

place

place-holder

point ,

polynomials in canonical form

positive definite formulae

precedence ,

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 ,

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 ,

rank function

re-initialize

read-only

read-only mode

recdef ,

record types

reducible attribute

referenced automatically

refinement

refiner

region

relation

equivalence

relation families

relations ,

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 ,

rhs ,

right-hand-side term

right to left

ring axioms

rnam

root goal

rule ,

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 ,

substitution ,

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 ,

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 ,

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 ,

termination characters

term sequence

term slots ,

terms with holes

Text Insertion

insert-spec-char-num

text sequence

text slot

text slots

text string

theorem

theorem

extraction

proof-script

theories ,

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 ,

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 ,

view function

visibility of the variable

visual presentation

well-formedness lemma

well-formedness theorems

whitespace

whitespace formatting

width

window

active

library , ,

multiple

Nuprl ,

proof

proof editor

refinement rule

rulebox

shell

term editor , ,

X

wrapper

see wrapped

xmiddle abstraction

yank-next in emacs

yank in emacs

Y combinator ,

zero width