src/Provers/classical.ML

   writeln"Safe introduction rules";  prths safeIs;
   writeln"Elimination rules";  prths hazEs;
   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, 
 	   safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper};