src/Provers/classical.ML
changeset 4625 9c6082518cfb
parent 4624 795b5b624c02
child 4646 f6298426f5a7
equal deleted inserted replaced
4624:795b5b624c02 4625:9c6082518cfb
   253 
   253 
   254 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   254 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   255   let val pretty_thms = map Display.pretty_thm in
   255   let val pretty_thms = map Display.pretty_thm in
   256     Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs));
   256     Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs));
   257     Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs));
   257     Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs));
   258     Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs))
   258     Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs));
   259     Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs));
   259     Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs))
   260   end;
   260   end;
   261 
   261 
   262 fun rep_claset (CS args) = args;
   262 fun rep_claset (CS args) = args;
   263 
   263 
   264 
   264