equal
deleted
inserted
replaced
43 val empty: expr |
43 val empty: expr |
44 datatype 'a element = Elem of 'a | Expr of expr |
44 datatype 'a element = Elem of 'a | Expr of expr |
45 val map_elem: ('a -> 'b) -> 'a element -> 'b element |
45 val map_elem: ('a -> 'b) -> 'a element -> 'b element |
46 |
46 |
47 val intern: theory -> xstring -> string |
47 val intern: theory -> xstring -> string |
|
48 val intern_expr: theory -> expr -> expr |
48 val extern: theory -> string -> xstring |
49 val extern: theory -> string -> xstring |
49 val init: string -> theory -> Proof.context |
50 val init: string -> theory -> Proof.context |
50 |
51 |
51 (* The specification of a locale *) |
52 (* The specification of a locale *) |
52 val parameters_of: theory -> string -> |
53 val parameters_of: theory -> string -> |