31 install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group)); |
31 install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group)); |
32 install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o |
32 install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o |
33 map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of)); |
33 map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of)); |
34 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm); |
34 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm); |
35 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm); |
35 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm); |
|
36 install_pp (make_pp ["Binding", "T"] (Pretty.pprint o Pretty.str o Binding.display)); |
36 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp); |
37 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp); |
37 install_pp (make_pp ["Context", "theory"] Context.pprint_thy); |
38 install_pp (make_pp ["Context", "theory"] Context.pprint_thy); |
38 install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref); |
39 install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref); |
39 install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context); |
40 install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context); |
40 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |
41 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |