equal
deleted
inserted
replaced
41 (term list list * (string * morphism) list * morphism) * Proof.context |
41 (term list list * (string * morphism) list * morphism) * Proof.context |
42 val sublocale: (local_theory -> local_theory) -> string -> expression_i -> |
42 val sublocale: (local_theory -> local_theory) -> string -> expression_i -> |
43 (Attrib.binding * term) list -> theory -> Proof.state |
43 (Attrib.binding * term) list -> theory -> Proof.state |
44 val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression -> |
44 val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression -> |
45 (Attrib.binding * string) list -> theory -> Proof.state |
45 (Attrib.binding * string) list -> theory -> Proof.state |
46 val interpretation: expression_i -> (Attrib.binding * term) list -> |
46 val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state |
47 theory -> Proof.state |
47 val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state |
48 val interpretation_cmd: expression -> (Attrib.binding * string) list -> |
48 val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state |
49 theory -> Proof.state |
|
50 val interpret: expression_i -> (Attrib.binding * term) list -> |
|
51 bool -> Proof.state -> Proof.state |
|
52 val interpret_cmd: expression -> (Attrib.binding * string) list -> |
49 val interpret_cmd: expression -> (Attrib.binding * string) list -> |
53 bool -> Proof.state -> Proof.state |
50 bool -> Proof.state -> Proof.state |
54 |
51 |
55 (* Diagnostic *) |
52 (* Diagnostic *) |
56 val print_dependencies: Proof.context -> bool -> expression -> unit |
53 val print_dependencies: Proof.context -> bool -> expression -> unit |