equal
deleted
inserted
replaced
14 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * Model.itm list * (bool * term) list |
14 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * Model.itm list * (bool * term) list |
15 val context_met : Celem.metID -> Ctree.ctree -> Pos.pos -> bool * Celem.metID * Program.T * Model.itm list * (bool * term) list |
15 val context_met : Celem.metID -> Ctree.ctree -> Pos.pos -> bool * Celem.metID * Program.T * Model.itm list * (bool * term) list |
16 val context_pbl : Celem.pblID -> Ctree.ctree -> Pos.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list |
16 val context_pbl : Celem.pblID -> Ctree.ctree -> Pos.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list |
17 val set_method : Celem.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
17 val set_method : Celem.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
18 val set_problem : Celem.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
18 val set_problem : Celem.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
19 val set_theory : ThyC.thyID -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
19 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
20 val tryrefine : Celem.pblID -> Ctree.ctree -> Pos.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list |
20 val tryrefine : Celem.pblID -> Ctree.ctree -> Pos.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list |
21 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
21 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
22 (*NONE*) |
22 (*NONE*) |
23 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
23 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
24 (*NONE*) |
24 (*NONE*) |