Next:
17. The IMPS Special
Up:
The IMPS User's Manual
Previous:
16. Syntax: Parsing and
3. Reference Manual
17. The IMPS Special Forms
17.1 Creating Objects
def-algebraic-processor
def-atomic-sort
def-bnf
def-cartesian-product
def-compound-macete
def-constant
def-imported-rewrite-rules
def-inductor
def-language
def-order-processor
def-primitive-recursive-constant
def-quasi-constructor
def-record-theory
def-recursive-constant
def-renamer
def-schematic-macete
def-script
def-section
def-sublanguage
def-theorem
def-theory
def-theory-ensemble
def-theory-ensemble-instances
def-theory-ensemble-multiple
def-theory-ensemble-overloadings
def-theory-instance
def-theory-processors
def-translation
def-transported-symbols
17.2 Changing Syntax
def-overloading
def-parse-syntax
def-print-syntax
17.3 Loading Sections and Files
load-section
include-files
17.4 Presenting Expressions
view-expr
18. The Proof Commands
Command Application in Interactive Mode
Command Application in Script Mode
antecedent-inference
antecedent-inference-strategy
apply-macete
apply-macete-locally
apply-macete-locally-with-minor-premises
apply-macete-with-minor-premises
assume-theorem
assume-transported-theorem
auto-instantiate-existential
auto-instantiate-universal-antecedent
backchain
backchain-backwards
backchain-repeatedly
backchain-through-formula
beta-reduce
beta-reduce-antecedent
beta-reduce-insistently
beta-reduce-repeatedly
beta-reduce-with-minor-premises
case-split
case-split-on-conditionals
choice-principle
contrapose
cut-using-sequent
cut-with-single-formula
definedness
direct-and-antecedent-inference-strategy
direct-and-antecedent-inference-strategy-with-
simplification
direct-inference
direct-inference-strategy
disable-quasi-constructor
edit-and-post-sequent-node
eliminate-defined-iota-expression
eliminate-iota
enable-quasi-constructor
extensionality
force-substitution
generalize-using-sequent
incorporate-antecedent
induction
insistent-direct-inference
insistent-direct-inference-strategy
instantiate-existential
instantiate-theorem
instantiate-transported-theorem
instantiate-universal-antecedent
instantiate-universal-antecedent-multiply
prove-by-logic-and-simplification
raise-conditional
simplify
simplify-antecedent
simplify-insistently
simplify-with-minor-premises
sort-definedness
sort-definedness-and-conditionals
unfold-defined-constants
unfold-defined-constants-repeatedly
unfold-directly-defined-constants
unfold-directly-defined-constants-repeatedly
unfold-recursively-defined-constants
unfold-recursively-defined-constants-repeatedly
unfold-single-defined-constant
unfold-single-defined-constant-globally
unordered-direct-inference
weaken
19. The Primitive Inference Procedures
antecedent-inference
backchain-inference
backchain-backwards-inference
backchain-through-formula-inference
choice
contraposition
cut
definedness
defined-constant-unfolding
direct-inference
disjunction-elimination
eliminate-iota
existential-generalization
extensionality
force-substitution
incorporate-antecedent
insistent-direct-inference
insistent-simplification
macete-application-at-paths
macete-application-with-minor-premises-at-paths
raise-conditional-inference
simplification
simplification-with-minor-premises
sort-definedness
theorem-assumption
universal-instantiation
unordered-conjunction-direct-inference
weakening
20. The Initial Theory Library: An Overview
§ abstract-calculus
§ banach-fixed-point-theorem
§ basic-cardinality
§ basic-fields
§ basic-group-theory
§ basic-monoids
§ binary-relations
§ binomial-theorem
§ counting-theorems-for-groups
§ foundation
§ groups-as-monoids
§ knaster-fixed-point-theorem
§ metric-spaces
§ metric-space-pairs
§ metric-space-continuity
§ number-theory
§ pairs
§ partial-orders
§ pre-reals
§ sequences
Glossary
Next:
17. The IMPS Special
Up:
The IMPS User's Manual
Previous:
16. Syntax: Parsing and
System Administrator
2000-07-19
