equal
deleted
inserted
replaced
607 fun put_claset cs = map_claset (K cs); |
607 fun put_claset cs = map_claset (K cs); |
608 |
608 |
609 fun print_claset ctxt = |
609 fun print_claset ctxt = |
610 let |
610 let |
611 val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; |
611 val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; |
612 val pretty_thms = map (Display.pretty_thm ctxt) o Item_Net.content; |
612 val pretty_thms = map (Pretty.item o single o Display.pretty_thm ctxt) o Item_Net.content; |
613 in |
613 in |
614 [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), |
614 [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), |
615 Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), |
615 Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), |
616 Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), |
616 Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), |
617 Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), |
617 Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), |