MEXPR : top-level command

Top Levels

• begin-prfw
• do-grades
• ed
• end-prfw
• history
• pop
• push
• review

Help

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

Collecting Help

• html-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

suggestions

• advice
• check-structure

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

RuleP

• rulep

Events

• disable-events

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

Lisp packages

• pack-stat
• unuse
• use

ETPS documentation homepage

TPS homepage