tuned print_cs;
authorwenzelm
Thu, 12 Feb 1998 16:38:08 +0100
changeset 4624 795b5b624c02
parent 4623 e6ada440a383
child 4625 9c6082518cfb
tuned print_cs;
src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Feb 12 15:43:50 1998 +0100
+++ b/src/Provers/classical.ML	Thu Feb 12 16:38:08 1998 +0100
@@ -253,10 +253,10 @@
 
 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   let val pretty_thms = map Display.pretty_thm in
-    Pretty.writeln (Pretty.big_list "introduction rules:" (pretty_thms hazIs));
     Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs));
-    Pretty.writeln (Pretty.big_list "elimination rules:" (pretty_thms hazEs));
+    Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs));
     Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs))
+    Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs));
   end;
 
 fun rep_claset (CS args) = args;