equal
deleted
inserted
replaced
26 ThyInfo.register_theory Pure.thy; |
26 ThyInfo.register_theory Pure.thy; |
27 |
27 |
28 |
28 |
29 (* ML toplevel pretty printing *) |
29 (* ML toplevel pretty printing *) |
30 |
30 |
|
31 install_pp (make_pp ["TaskQueue", "task"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_task)); |
|
32 install_pp (make_pp ["TaskQueue", "group"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_group)); |
31 install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o |
33 install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o |
32 map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of)); |
34 map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of)); |
33 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm); |
35 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm); |
34 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm); |
36 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm); |
35 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp); |
37 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp); |