next up previous contents
Next: Printing Transcripts Up: Reference Material for Tutorial Previous: ML Functions for ML

Tactics


 

 

Table 4: Tactics
D i Decompose
  1.hyps ($i\gt$): and, or, implies, not, exists
  2.concl (i=0 ): and, implies, all, not
ID i Decompose implies, not, all in hyp without thinning
Sel n (D 0) Decompose or in concl. (n=1,2 )
With t (D i ) Instantiate with term t
  1. all in hyp 2. exists in concl
UnivCD D 0 on implies, all
GenUnivCD D 0 on implies, all, and
ClassDecide P Case split on whether P or $\neg P$ is true
Trivial 1. true in concl.
  2. false in hyp.
  3. P and $\neg P$ in hyps.
  4. P in concl and some hyp.
Auto Solve goals of form $t\ \in\ T$.
T1 THENM T2 Run T1 , then T2 on main subgoals
T1 THENW T2 Run T1 , then T2 on wf subgoals

Some useful tactics are summarized in Table 4.

next up previous contents
Next: Printing Transcripts Up: Reference Material for Tutorial Previous: ML Functions for ML
Dora Abdullah, 12/4/97