equal
deleted
inserted
replaced
214 val it = ("x=-#5//#12","") : string * string*) |
214 val it = ("x=-#5//#12","") : string * string*) |
215 |
215 |
216 |
216 |
217 |
217 |
218 |
218 |
219 (*.applicability of a tacic wrt. a calc-state (ptree,pos'). |
219 (*.applicability of a tacic wrt. a calc-state (ctree,pos'). |
220 additionally used by next_tac in the script-interpreter for script-tacs. |
220 additionally used by next_tac in the script-interpreter for script-tacs. |
221 tests for applicability are so expensive, that results (rewrites!) |
221 tests for applicability are so expensive, that results (rewrites!) |
222 are kept in the return-value of 'type tac_'. |
222 are kept in the return-value of 'type tac_'. |
223 .*) |
223 .*) |
224 fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = Chead.Appl (Init_Proof' (ct', spec)) |
224 fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = Chead.Appl (Init_Proof' (ct', spec)) |