src/Provers/classical.ML
changeset 51580 64ef8260dc60
parent 50112 11cd86c5af3a
child 51584 98029ceda8ce
equal deleted inserted replaced
51579:ec3b78ce0758 51580:64ef8260dc60
   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),