[isabelle-dev] NEWS

Makarius makarius at sketis.net
Thu Sep 18 20:12:48 CEST 2008

* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
to 'a -> thm, while results are always tagged with an authentic oracle
name.  The Isar command 'oracle' is now polymorphic, no argument type
is specified.  INCOMPATIBILITY, need to simplify existing oracle code
accordingly.  Note that extra performance may be gained by producing
the cterm carefully, avoiding slow Thm.cterm_of.

More information about the isabelle-dev mailing list