equal
deleted
inserted
replaced
77 (** pretty printing **) |
77 (** pretty printing **) |
78 |
78 |
79 fun pretty_ss ctxt ss = |
79 fun pretty_ss ctxt ss = |
80 let |
80 let |
81 val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of; |
81 val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of; |
82 val pretty_thm = ProofContext.pretty_thm ctxt; |
82 val pretty_thm = Display.pretty_thm ctxt; |
83 fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss); |
83 fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss); |
84 fun pretty_cong (name, thm) = |
84 fun pretty_cong (name, thm) = |
85 Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm]; |
85 Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm]; |
86 |
86 |
87 val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss; |
87 val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss; |