Re: [isabelle] Status of "eval" method

> a student of mine recently noticed that there is no documentation for
> the "eval" method. Nevertheless, he was able to find it. What he of
> course did not recognize was, that it actually seems to "prove" theorems
> by cheating (they are pretty-printed with [!] afterwards). 
> So I propose to either add proper documentation for this method,
> including a warning that it does not go through the inference kernel,
> perhaps even renaming it to something like "eval_sorry", or to remove
> it.

»eval« is the successor of the »evaluation« method, which wasn't ever
documented thoroughly either (at least I guess so, otherwise I would
have migrated that documentation).

If all methods relying on oracles are supposed to reflect this in their
name, there are a couple of other candidates also, e.g. normalizsation.
 Keep this in mind when discussing renames etc.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.