author | lcp |
Thu, 06 Apr 1995 11:55:51 +0200 | |
changeset 1010 | a7693f30065d |
parent 1009 | eb7c50688405 |
child 1011 | 5c9654e2e3de |
--- 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,