[isabelle] Status of "eval" method



Hi,

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.

--
  Peter







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