equal
deleted
inserted
replaced
9 sig |
9 sig |
10 type context |
10 type context |
11 exception CONTEXT of string * context |
11 exception CONTEXT of string * context |
12 val theory_of: context -> theory |
12 val theory_of: context -> theory |
13 val sign_of: context -> Sign.sg |
13 val sign_of: context -> Sign.sg |
|
14 val prems_of: context -> thm list |
14 val show_hyps: bool ref |
15 val show_hyps: bool ref |
15 val pretty_thm: thm -> Pretty.T |
16 val pretty_thm: thm -> Pretty.T |
16 val verbose: bool ref |
17 val verbose: bool ref |
17 val print_binds: context -> unit |
18 val print_binds: context -> unit |
18 val print_thms: context -> unit |
19 val print_thms: context -> unit |