119 |
119 |
120 fun pretty_ss ctxt ss = |
120 fun pretty_ss ctxt ss = |
121 let |
121 let |
122 val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of; |
122 val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of; |
123 val pretty_thm = Display.pretty_thm ctxt; |
123 val pretty_thm = Display.pretty_thm ctxt; |
124 fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss); |
124 fun pretty_proc (name, lhss) = |
|
125 Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss); |
125 fun pretty_cong (name, thm) = |
126 fun pretty_cong (name, thm) = |
126 Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm]; |
127 Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm]; |
127 |
128 |
128 val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss; |
129 val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss; |
129 in |
130 in |
130 [Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps), |
131 [Pretty.big_list "simplification rules:" (map (Pretty.item o single o pretty_thm o #2) simps), |
131 Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)), |
132 Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)), |
132 Pretty.big_list "congruences:" (map pretty_cong congs), |
133 Pretty.big_list "congruences:" (map pretty_cong congs), |
133 Pretty.strs ("loopers:" :: map quote loopers), |
134 Pretty.strs ("loopers:" :: map quote loopers), |
134 Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers), |
135 Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers), |
135 Pretty.strs ("safe solvers:" :: map quote safe_solvers)] |
136 Pretty.strs ("safe solvers:" :: map quote safe_solvers)] |