changeset 3871 | 8b1b0d493ca9 |
parent 3857 | 16198fde5af5 |
child 3901 | 8b09bc500f65 |
--- a/NEWS Wed Oct 15 11:27:55 1997 +0200 +++ b/NEWS Wed Oct 15 11:43:27 1997 +0200 @@ -33,6 +33,9 @@ * deleted the obsolete tactical STATE, which was declared by fun STATE tacfun st = tacfun st st; +* slightly changed interfaces for oracles: admit many per theory, named +(e.g. oracle foo = mlfun), additional name argument for invoke_oracle; + *** Classical Reasoner ***