# HG changeset patch
# User wenzelm
# Date 967673709 -7200
# Node ID 72c0a12ae3bf4ddbe41d61a2749ddcc7005d5643
# Parent  8e835ebc862f862da7e64d075a89535012c0a9fa
improved messages;

diff -r 8e835ebc862f -r 72c0a12ae3bf src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Aug 31 00:11:40 2000 +0200
+++ b/src/Provers/classical.ML	Thu Aug 31 00:15:09 2000 +0200
@@ -272,12 +272,12 @@
 
 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) =
   let val pretty_thms = map Display.pretty_thm in
-    [Pretty.big_list "safe introduction rules:" (pretty_thms safeIs),
-      Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs),
-      Pretty.big_list "extra introduction rules:" (pretty_thms xtraIs),
-      Pretty.big_list "safe elimination rules:" (pretty_thms safeEs),
-      Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs),
-      Pretty.big_list "extra elimination rules:" (pretty_thms xtraEs)]
+    [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
+      Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
+      Pretty.big_list "extra introduction rules (intro?):" (pretty_thms xtraIs),
+      Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
+      Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
+      Pretty.big_list "extra elimination rules (elim?):" (pretty_thms xtraEs)]
     |> Pretty.chunks |> Pretty.writeln
   end;
 
@@ -331,9 +331,9 @@
   else if mem_thm (th, safeEs) then
          warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
   else if mem_thm (th, hazIs) then 
-         warning ("Rule already declared as unsafe introduction (intro)\n" ^ string_of_thm th)
+         warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th)
   else if mem_thm (th, hazEs) then 
-         warning ("Rule already declared as unsafe elimination (elim)\n" ^ string_of_thm th)
+         warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th)
   else if mem_thm (th, xtraIs) then 
          warning ("Rule already declared as extra introduction (intro?)\n" ^ string_of_thm th)
   else if mem_thm (th, xtraEs) then 
@@ -410,7 +410,7 @@
 		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
 	  th)=
   if mem_thm (th, hazIs) then 
-	 (warning ("Ignoring duplicate unsafe introduction (intro)\n" ^ string_of_thm th);
+	 (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
 	  cs)
   else
   let val nI = length hazIs + 1
@@ -435,7 +435,7 @@
 		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
 	  th) =
   if mem_thm (th, hazEs) then 
-	 (warning ("Ignoring duplicate unsafe elimination (elim)\n" ^ string_of_thm th);
+	 (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
 	  cs)
   else
   let val nI = length hazIs