

	How to give a tactic tree demo. 

Suppose that the tactic tree code is in directory EXENE-DIR. 

Documentation can be found in EXENE-DIR/demos/tactic-tree/doc/doc.ps. 

Here is how to get started with a demo: 

% eXene 

- System.Directory.cd "EXENE-DIR/demos/tactic-tree/src";
- use "load";
- System.Directory.cd "../examples/fol";
- use "load-fol";

This will leave you with two functions, 

val create : string * string * (string * tactic) list -> ttree_state
val view : ttree_state * string * (string * tactic) list -> ttree_state

and some example formulas, 

val p1 = "A' -> B' -> (A' & B')" : string
val p2 = "A' -> B' -> C' -> ((A' & B') & (B' & C'))" : string
val p3 = " (P' -> (Q' | R')) -> ((P' ->Q') | (P' ->R'))" : string
val p4 = "((A' | B') -> C') -> ((A' -> C') & (B' -> C'))" : string

To prove p4, enter 

- val p = create(p4,"",[]) ;

this will pop up a tactic tree window (on display "", the current display, with 
an empty list of auxiliary tactics). 

Upon exiting the tactic tree window, p is bound to a tactic tree state. 
This state can be revisited by 

- view(p,"",[]) ; 


