equal
deleted
inserted
replaced
7 |
7 |
8 signature THEORY_STORE_READ = |
8 signature THEORY_STORE_READ = |
9 sig |
9 sig |
10 val thy_containing_thm : string -> string * string |
10 val thy_containing_thm : string -> string * string |
11 val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id |
11 val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id |
12 val thy_containing_cal : ThyC.id -> Eval_Def.prog_calcID -> string * string |
12 val thy_containing_cal : ThyC.id -> Eval_Def.prog_id -> string * string |
13 |
13 |
14 val from_store : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *) |
14 val from_store : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *) |
15 \<^isac_test>\<open> |
15 \<^isac_test>\<open> |
16 val isabthys: unit -> theory list |
16 val isabthys: unit -> theory list |
17 val knowthys: unit -> theory list |
17 val knowthys: unit -> theory list |