Am 01.07.2014 um 19:45 schrieb Makarius :
> * src/HOL/Tools/ATP/atp_problem_generate.ML
>
>Two occurrences that are not immediately clear. Looks like plain
>structural equality could do the job.
Right. This looks like very minor optimizations. I'm taking them out (pushed to
testboard
On Tue, 25 Mar 2014, Makarius wrote:
* pointer_eq is not part of SML and requires extra reasoning that it is
correct whenever it is used (normally in certain hot-spots of kernel
operations). See also the surprise caused by some optimizations of
the Poly/ML runtime system concernin
Here are some cumulative notes on Isabelle/ML wrt. current
Isabelle/20cf88cd3188, about new and old things.
* The configuration options ML_source_trace, ML_exception_trace,
ML_print_depth control various aspects of ML compilation and run-time
within the regular context -- as usual in a
