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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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