equal
deleted
inserted
replaced
5 Common theory/locale/class/instantiation/overloading targets. |
5 Common theory/locale/class/instantiation/overloading targets. |
6 *) |
6 *) |
7 |
7 |
8 signature THEORY_TARGET = |
8 signature THEORY_TARGET = |
9 sig |
9 sig |
10 val peek: local_theory -> |
10 val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} |
11 {target: string, |
|
12 is_locale: bool, |
|
13 is_class: bool} |
|
14 val init: string option -> theory -> local_theory |
11 val init: string option -> theory -> local_theory |
15 val context_cmd: xstring -> theory -> local_theory |
12 val context_cmd: xstring -> theory -> local_theory |
16 val instantiation: string list * (string * sort) list * sort -> theory -> local_theory |
13 val instantiation: string list * (string * sort) list * sort -> theory -> local_theory |
17 val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory |
14 val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory |
18 val overloading: (string * (string * typ) * bool) list -> theory -> local_theory |
15 val overloading: (string * (string * typ) * bool) list -> theory -> local_theory |