MEXPR : top-level command

Top Levels

• begin-prfw
• do-grades
• ed
• end-prfw
• history
• lib
• mate
• mtree
• pop
• push
• review
• test
• uniform-search
• uniform-search-l
• unify

Help

• ?
• ??
• abbreviations
• environment
• help
• help*
• help-group
• list-rules
• oops
• problems
• search

Collecting Help

• chardoc
• collect-help
• help-list
• html-doc
• quick-ref
• scribe-doc

Concept

• loadkey
• reset

Starting and Finishing

• alias
• cleanup
• done
• exercise
• exit
• news
• prove
• reconsider
• remark
• summary
• unalias

Printing

• build-proof-hierarchy
• depth
• explain
• find-line
• pall
• pbrief
• pl
• pl*
• pline
• pplan
• print-proof-structure
• prw
• pw
• pwscope
• pwtypes
• shownotypes
• showtypes
• tableau
• ^p
• ^pn

Saving Work

• execute-file
• findproof
• finish-save
• pause
• restore-work
• restoreproof
• resume-save
• save-flags-and-work
• save-subproof
• save-work
• saveproof
• script
• stop-save
• unscript

Saving Wffs

• append-wff
• append-wffs

Printing Proofs into Files

• printproof
• scribeproof
• setup-slide-style
• slideproof
• texproof

Proof Outline

• create-subproof
• line-comment
• merge-proofs
• proof-comment
• prooflist
• transfer-lines

Search Suggestions

• auto-suggest
• etr-auto-suggest

Mating search

• close-testwin
• diy
• diy-l
• monitor
• monitorlist
• nomonitor

MS91-6 and MS91-7 search procedures

• search-order

Proof Translation

• etree-nat
• nat-etree
• nat-etree-old
• pfnat
• pntr
• tidy-proof

Unification

• least-search-depth

Tactics

• echo
• use-tactic

suggestions

• advice
• check-structure
• go
• go2
• monstro
• suggest

Vpforms

• close-matevpw
• open-matevpw

Rearranging the Proof

• add-hyps
• delete
• delete*
• delete-hyps
• introduce-gap
• lock-line
• modify-gaps
• move
• move*
• plan
• renumberall
• squeeze
• unlock-line

Status

• are-we-using
• count-lines
• pstatus
• sponsor
• subproof
• unsponsor

Miscellaneous Rules

• assert
• hyp
• lemma
• same

Propositional Rules

• assoc-left
• cases
• cases3
• cases4
• deduct
• disj-imp
• disj-imp-l
• disj-imp-r
• econj
• equiv-implics
• iconj
• idisj-left
• idisj-right
• imp-disj
• imp-disj-l
• imp-disj-r
• implics-equiv
• indirect
• indirect1
• indirect2
• mp
• rulec1
• subst-equiv

Negation Rules

• absurd
• eneg
• ineg
• pullneg
• pushneg

Quantifier Rules

• ab*
• abe
• abu
• egen
• rulec
• ugen
• ui

Substitution Rules

• substitute
• typesubst

Equality Rules

• equiv-eq
• equiv-eq-contr
• equiv-eq-contr*
• equiv-eq-expd
• equiv-eq-expd*
• ext=
• ext=0
• let
• subst=
• subst=l
• subst=r
• sym=

Definition Rules

• edef
• equiv-wffs
• idef

Lambda Conversion Rules

• beta*
• eta*
• lambda*
• lcontr*
• lcontr*-beta
• lcontr*-eta
• lexpd*
• lexpd*-beta
• lexpd*-eta

Rewriting commands

• activate-rules
• deactivate-rules
• delete-rrule
• list-rrules
• make-abbrev-rrule
• make-inverse-rrule
• make-theory
• permute-rrules
• rewrite-supp*
• rewrite-supp1
• simplify-plan
• simplify-plan*
• simplify-supp
• simplify-supp*
• unrewrite-plan*
• unrewrite-plan1
• use-rrules
• use-theory

RuleP

• rulep

Events

• disable-events

Statistics

• daterec
• display-time

Maintenance

• cload
• cload-modules
• compile-list
• compl
• filetype
• ledit
• load-slow
• organize
• qload
• sys-load
• test-init
• tlist
• tload
• tps-test
• tps-test2
• tps3-save

Modules

• loaded-mods
• modules
• unloaded-mods

Rules Module

• assemble-file
• assemble-mod
• build
• write-rule

Lisp packages

• pack-stat
• unuse
• use

Display

• displayfile

Best modes

• moderec

Bugs

• bug-delete
• bug-help
• bug-list
• bug-restore
• bug-save

TPS documentation homepage

TPS homepage