equal
deleted
inserted
replaced
26 val itms2itemppc : theory -> Model.itm list -> (bool * term) list -> Model.item Model.ppc (* for generate.sml *) |
26 val itms2itemppc : theory -> Model.itm list -> (bool * term) list -> Model.item Model.ppc (* for generate.sml *) |
27 |
27 |
28 val get_pbt : Problem.id -> Problem.T |
28 val get_pbt : Problem.id -> Problem.T |
29 val get_met : Method.id -> Method.T (* for generate.sml *) |
29 val get_met : Method.id -> Method.T (* for generate.sml *) |
30 val get_met' : theory -> Method.id -> Method.T (* for pbl-met-hierarchy.sml *) |
30 val get_met' : theory -> Method.id -> Method.T (* for pbl-met-hierarchy.sml *) |
31 val get_the : Thy_Html.theID -> Thy_Html.thydata (* for inform.sml *) |
31 val get_the : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *) |
32 |
32 |
33 type pblRD = string list (* for pbl-met-hierarchy.sml *) |
33 type pblRD = string list (* for pbl-met-hierarchy.sml *) |
34 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *) |
34 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *) |
35 val scan : string list -> 'a Store.T -> string list list (* for thy-hierarchy.sml *) |
35 val scan : string list -> 'a Store.T -> string list list (* for thy-hierarchy.sml *) |
36 val itm_out : theory -> Model.itm_ -> string |
36 val itm_out : theory -> Model.itm_ -> string |