equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 install_pp (make_pp ["Thm", "thm"] pprint_thm); |
7 install_pp (make_pp ["Thm", "thm"] pprint_thm); |
8 install_pp (make_pp ["Thm", "theory"] pprint_theory); |
8 install_pp (make_pp ["Thm", "theory"] pprint_theory); |
9 install_pp (make_pp ["Sign", "sg"] pprint_sg); |
9 install_pp (make_pp ["Sign", "sg"] pprint_sg); |
10 install_pp (make_pp ["term"] pprint_term); |
|
11 install_pp (make_pp ["Sign", "cterm"] Sign.pprint_cterm); |
10 install_pp (make_pp ["Sign", "cterm"] Sign.pprint_cterm); |
12 install_pp (make_pp ["typ"] pprint_typ); |
|
13 install_pp (make_pp ["Sign", "ctyp"] Sign.pprint_ctyp); |
11 install_pp (make_pp ["Sign", "ctyp"] Sign.pprint_ctyp); |
14 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |
12 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |
15 |
13 |
|
14 (* |
|
15 install_pp (make_pp ["term"] pprint_term); |
|
16 install_pp (make_pp ["typ"] pprint_typ); |
|
17 *) |