equal
deleted
inserted
replaced
48 val markup_type: Proof.context -> string -> string |
48 val markup_type: Proof.context -> string -> string |
49 val pretty_type: Proof.context -> string -> Pretty.T |
49 val pretty_type: Proof.context -> string -> Pretty.T |
50 val extern_const: Proof.context -> string -> xstring |
50 val extern_const: Proof.context -> string -> xstring |
51 val markup_const: Proof.context -> string -> string |
51 val markup_const: Proof.context -> string -> string |
52 val pretty_const: Proof.context -> string -> Pretty.T |
52 val pretty_const: Proof.context -> string -> Pretty.T |
53 val transfer_syntax: theory -> Proof.context -> Proof.context |
|
54 val transfer: theory -> Proof.context -> Proof.context |
53 val transfer: theory -> Proof.context -> Proof.context |
55 val background_theory: (theory -> theory) -> Proof.context -> Proof.context |
54 val background_theory: (theory -> theory) -> Proof.context -> Proof.context |
56 val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context |
55 val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context |
57 val extern_fact: Proof.context -> string -> xstring |
56 val extern_fact: Proof.context -> string -> xstring |
58 val pretty_term_abbrev: Proof.context -> term -> Pretty.T |
57 val pretty_term_abbrev: Proof.context -> term -> Pretty.T |