# HG changeset patch
# User wenzelm
# Date 965847563 -7200
# Node ID 216d053992a568623d98660fafd1efef43ca9625
# Parent  6b07b56aa3a8a74b5968135b7148cda73ee0cc34
fixed classification of rules in atts and modifiers (final!?);

diff -r 6b07b56aa3a8 -r 216d053992a5 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Aug 09 20:46:58 2000 +0200
+++ b/src/Provers/classical.ML	Wed Aug 09 20:59:23 2000 +0200
@@ -6,7 +6,7 @@
 Theorem prover for classical reasoning, including predicate calculus, set
 theory, etc.
 
-Rules must be classified as intr, elim, safe, hazardous (unsafe).
+Rules must be classified as intro, elim, safe, hazardous (unsafe).
 
 A rule is unsafe unless it can be applied blindly without harmful results.
 For a rule to be safe, its premises and conclusion should be logically
@@ -346,7 +346,7 @@
 	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
 	   th)  =
   if mem_thm (th, safeIs) then 
-	 (warning ("Ignoring duplicate Safe Intr\n" ^ string_of_thm th);
+	 (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
 	  cs)
   else
   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
@@ -373,7 +373,7 @@
 		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
 	   th)  =
   if mem_thm (th, safeEs) then 
-	 (warning ("Ignoring duplicate Safe Elim\n" ^ string_of_thm th);
+	 (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
 	  cs)
   else
   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
@@ -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 Intr\n" ^ string_of_thm th);
+	 (warning ("Ignoring duplicate unsafe 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 Elim\n" ^ string_of_thm th);
+	 (warning ("Ignoring duplicate unsafe elimination (elim)\n" ^ string_of_thm th);
 	  cs)
   else
   let val nI = length hazIs 
@@ -468,7 +468,7 @@
 		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
 	  th)=
   if mem_thm (th, xtraIs) then 
-	 (warning ("Ignoring duplicate extra Intr\n" ^ string_of_thm th);
+	 (warning ("Ignoring duplicate extra introduction (intro?)\n" ^ string_of_thm th);
 	  cs)
   else
   let val nI = length xtraIs + 1
@@ -493,7 +493,7 @@
 		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
 	  th) =
   if mem_thm (th, xtraEs) then
-	 (warning ("Ignoring duplicate extra Elim\n" ^ string_of_thm th);
+	 (warning ("Ignoring duplicate extra elimination (elim?)\n" ^ string_of_thm th);
 	  cs)
   else
   let val nI = length xtraIs 
@@ -1035,7 +1035,7 @@
 val bang_colon = Args.$$$ "!:";
 
 fun cla_att change xtra haz safe = Attrib.syntax
-  (Scan.lift ((query >> K xtra || bang >> K haz || Scan.succeed safe) >> change));
+  (Scan.lift ((query >> K xtra || bang >> K safe || Scan.succeed haz) >> change));
 
 fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
 val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local);
@@ -1147,14 +1147,14 @@
 
 val cla_modifiers =
  [Args.$$$ destN -- query_colon >> K ((I, xtra_dest_local):Method.modifier),
-  Args.$$$ destN -- bang_colon >> K (I, haz_dest_local),
-  Args.$$$ destN -- colon >> K (I, safe_dest_local),
+  Args.$$$ destN -- bang_colon >> K (I, safe_dest_local),
+  Args.$$$ destN -- colon >> K (I, haz_dest_local),
   Args.$$$ elimN -- query_colon >> K (I, xtra_elim_local),
-  Args.$$$ elimN -- bang_colon >> K (I, haz_elim_local),
-  Args.$$$ elimN -- colon >> K (I, safe_elim_local),
+  Args.$$$ elimN -- bang_colon >> K (I, safe_elim_local),
+  Args.$$$ elimN -- colon >> K (I, haz_elim_local),
   Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
-  Args.$$$ introN -- bang_colon >> K (I, haz_intro_local),
-  Args.$$$ introN -- colon >> K (I, safe_intro_local),
+  Args.$$$ introN -- bang_colon >> K (I, safe_intro_local),
+  Args.$$$ introN -- colon >> K (I, haz_intro_local),
   Args.$$$ delN -- colon >> K (I, delrule_local)];
 
 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>