Re: [isabelle] Status of "eval" method

Am 17.10.2012 um 11:20 schrieb Makarius:

> "eval_sorry" would indeed be a rather odd name, because it is based on a different oracle that is supposed to be correct relative to the implementation of the code generator.

But what about "eval_oracle"? It would minimize the risk that somebody misunderstood its nature (and would free up a useful name, "eval", for the non-oracle version if desired).


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