equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 signature CLASS = |
7 signature CLASS = |
8 sig |
8 sig |
9 include CLASS_TARGET |
9 include CLASS_TARGET |
10 (*FIXME the split into class_target.ML, Named_Target.ML and |
10 (*FIXME the split into class_target.ML, named_target.ML and |
11 class.ML is artificial*) |
11 class.ML is artificial*) |
12 |
12 |
13 val class: binding -> class list -> Element.context_i list |
13 val class: binding -> class list -> Element.context_i list |
14 -> theory -> string * local_theory |
14 -> theory -> string * local_theory |
15 val class_cmd: binding -> xstring list -> Element.context list |
15 val class_cmd: binding -> xstring list -> Element.context list |