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