Re: [isabelle] Status of "eval" method
A thorough documentation can be found in the code generation tutorial in
If you care much about evaluations going through Isabelle's inference
kernel, Isabelle provides a method "code_simp", which does the same as
eval but slower ;)
Maybe you could add documentation about eval in the Isar reference (by
extending chapter 10.20) then, and summarize the proof methods of chapter 6?
Removing is not possible as the Flyspeck proof relies on this method.
In my opinion, renaming is not a reasonable option either.
On 10/17/2012 09:36 AM, Peter Lammich wrote:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and