author | wenzelm |
Wed, 26 Jul 2006 00:44:44 +0200 | |
changeset 20207 | 4c57e850e8d5 |
parent 18800 | c0f90bbf3865 |
child 20211 | c7f907f41f7c |
permissions | -rw-r--r-- |
(* Title: Pure/install_pp.ML ID: $Id$ ML toplevel pretty printing. *) install_pp (make_pp ["Thm", "thm"] Display.pprint_thm); install_pp (make_pp ["Thm", "cterm"] Display.pprint_cterm); install_pp (make_pp ["Thm", "ctyp"] Display.pprint_ctyp); install_pp (make_pp ["Context", "theory"] Context.pprint_thy); install_pp (make_pp ["Context", "proof"] ProofContext.pprint_context); install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); install_pp (make_pp ["typ"] (Sign.pprint_typ ProtoPure.thy));