26 val set_theory : Rule.thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd |
26 val set_theory : Rule.thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd |
27 val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list |
27 val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list |
28 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
28 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
29 val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tactic.input) * Telem.safe * Ctree.ctree |
29 val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tactic.input) * Telem.safe * Ctree.ctree |
30 val f2str : Generate.mout -> Rule.cterm' |
30 val f2str : Generate.mout -> Rule.cterm' |
31 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*) |
31 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
32 type nxt_ |
32 type nxt_ |
33 datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate' |
33 datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate' |
34 val loc_solve_ : string * Tactic.T -> Ctree.ctree * Ctree.pos' -> lOc_ |
34 val loc_solve_ : string * Tactic.T -> Ctree.ctree * Ctree.pos' -> lOc_ |
35 val loc_specify_ : Tactic.T -> Ctree.state -> lOc_ |
35 val loc_specify_ : Tactic.T -> Ctree.state -> lOc_ |
36 val nxt_specify_: Ctree.ctree * Ctree.pos' -> Chead.calcstate' |
36 val nxt_specify_: Ctree.ctree * Ctree.pos' -> Chead.calcstate' |
37 val TESTg_form : Ctree.state -> Generate.mout |
37 val TESTg_form : Ctree.state -> Generate.mout |
38 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
39 |
39 |
40 (*----- unused code, kept as hints to design ideas ---------------------------------------------*) |
40 (*----- unused code, kept as hints to design ideas ---------------------------------------------*) |
41 (* NONE *) |
41 (* NONE *) |
42 end |
42 end |
43 |
43 |