NEWS
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 ***