| author | haftmann |
| Mon, 10 Apr 2006 08:30:26 +0200 | |
| changeset 19398 | 8ad34412ea97 |
| parent 18800 | c0f90bbf3865 |
| child 20211 | c7f907f41f7c |
| permissions | -rw-r--r-- |
| 19 | 1 |
(* Title: Pure/install_pp.ML |
| 0 | 2 |
ID: $Id$ |
3 |
||
|
16438
1093f2400411
removed obsolete pretty printers for Theory.theory, Sign.sg;
wenzelm
parents:
16355
diff
changeset
|
4 |
ML toplevel pretty printing. |
| 0 | 5 |
*) |
6 |
||
| 11885 | 7 |
install_pp (make_pp ["Thm", "thm"] Display.pprint_thm); |
8 |
install_pp (make_pp ["Thm", "cterm"] Display.pprint_cterm); |
|
9 |
install_pp (make_pp ["Thm", "ctyp"] Display.pprint_ctyp); |
|
|
16438
1093f2400411
removed obsolete pretty printers for Theory.theory, Sign.sg;
wenzelm
parents:
16355
diff
changeset
|
10 |
install_pp (make_pp ["Context", "theory"] Context.pprint_thy); |
|
18800
c0f90bbf3865
added ProofContext.pprint_context (depends on ProofContext.debug);
wenzelm
parents:
16596
diff
changeset
|
11 |
install_pp (make_pp ["Context", "proof"] ProofContext.pprint_context); |
| 3509 | 12 |
install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |
|
16596
81ea5a085158
replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);
wenzelm
parents:
16438
diff
changeset
|
13 |
install_pp (make_pp ["typ"] (Sign.pprint_typ ProtoPure.thy)); |