equal
deleted
inserted
replaced
133 or left/right-hand-side of eqality .*) |
133 or left/right-hand-side of eqality .*) |
134 eval_fn |
134 eval_fn |
135 | Rls_ of rls (*.ie. rule sets may be nested.*) |
135 | Rls_ of rls (*.ie. rule sets may be nested.*) |
136 and scr = |
136 and scr = |
137 EmptyScr |
137 EmptyScr |
138 | Prog of term (* for met *) |
138 | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr' |
|
139 where 'exp' does not contain a tactic. *) |
139 | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *) |
140 | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *) |
140 {init_state : (* initialise for reverse rewriting by the Interpreter *) |
141 {init_state : (* initialise for reverse rewriting by the Interpreter *) |
141 term -> (* for this the rrlsstate is initialised: *) |
142 term -> (* for this the rrlsstate is initialised: *) |
142 term * (* the current formula: goes locate_gen -> next_tac via istate *) |
143 term * (* the current formula: goes locate_gen -> next_tac via istate *) |
143 term * (* the final formula *) |
144 term * (* the final formula *) |