# HG changeset patch
# User lcp
# Date 797162151 -7200
# Node ID a7693f30065dfe53123a73969c3ceaf6500d8936
# Parent  eb7c5068840555f18c3bf4fa6a0724a82c01e3b5
Added comment.

diff -r eb7c50688405 -r a7693f30065d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Apr 06 11:14:51 1995 +0200
+++ b/src/Provers/classical.ML	Thu Apr 06 11:55:51 1995 +0200
@@ -176,7 +176,9 @@
   writeln"Safe elimination rules";  prths safeEs;
   ());
 
-(** Adding new (un)safe introduction or elimination rules **)
+(** Adding new (un)safe introduction or elimination rules 
+    In case of overlap, new rules are tried BEFORE old ones
+**)
 
 fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addSIs ths =
   make_cs {safeIs=ths@safeIs,