# HG changeset patch
# User wenzelm
# Date 876908607 -7200
# Node ID 8b1b0d493ca928c172b648fcdd77b43ad3ac2d7b
# Parent  6913700d7c7995d0a7be7ac89d99bade0e0c17df
slightly changed interfaces for oracles;

diff -r 6913700d7c79 -r 8b1b0d493ca9 NEWS
--- 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 ***