equal
deleted
inserted
replaced
62 |
62 |
63 val _ = |
63 val _ = |
64 register "context" "context of local theory target" Toplevel.pretty_context; |
64 register "context" "context of local theory target" Toplevel.pretty_context; |
65 |
65 |
66 val _ = |
66 val _ = |
67 register "cases" "cases of proof context" (Proof_Context.pretty_cases o Toplevel.context_of); |
67 register "cases" "cases of proof context" |
|
68 (Proof_Context.pretty_cases o Toplevel.context_of); |
68 |
69 |
69 val _ = |
70 val _ = |
70 register "terms" "term bindings of proof context" |
71 register "terms" "term bindings of proof context" |
71 (Proof_Context.pretty_term_bindings o Toplevel.context_of); |
72 (Proof_Context.pretty_term_bindings o Toplevel.context_of); |
72 |
73 |
73 val _ = |
74 val _ = |
74 register "theorems" "theorems of local theory or proof context" |
75 register "theorems" "theorems of local theory or proof context" |
75 (single o Isar_Cmd.pretty_theorems false); |
76 (Isar_Cmd.pretty_theorems false); |
76 |
77 |
77 val _ = |
78 val _ = |
78 register "state" "proof state" Toplevel.pretty_state; |
79 register "state" "proof state" Toplevel.pretty_state; |
79 |
80 |
80 end; |
81 end; |