changeset 3968 | ec138de716d9 |
parent 3964 | f95d2fb6fac8 |
child 3982 | 2a903ba8d39e |
--- a/NEWS Tue Oct 21 18:09:13 1997 +0200 +++ b/NEWS Tue Oct 21 18:15:43 1997 +0200 @@ -28,6 +28,9 @@ restricted to 'trivial' ones, thus one may have to use transfer:theory->thm->thm in (rare) cases; +* improved handling of draft signatures / theories; draft thms (and +ctyps, cterms) are automatically promoted to real ones; + * slightly changed interfaces for oracles: admit many per theory, named (e.g. oracle foo = mlfun), additional name argument for invoke_oracle;