equal
deleted
inserted
replaced
666 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous |
666 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous |
667 quasi-bound variables (like the Simplifier), instead of accidentally |
667 quasi-bound variables (like the Simplifier), instead of accidentally |
668 named local fixes. This has the potential to improve stability of proof |
668 named local fixes. This has the potential to improve stability of proof |
669 tools, but can also cause INCOMPATIBILITY for tools that don't observe |
669 tools, but can also cause INCOMPATIBILITY for tools that don't observe |
670 the proof context discipline. |
670 the proof context discipline. |
|
671 |
|
672 * The following combinators for low-level profiling of the ML runtime |
|
673 system are available: |
|
674 |
|
675 profile_time (*CPU time*) |
|
676 profile_time_thread (*CPU time on this thread*) |
|
677 profile_allocations (*overall heap allocations*) |
671 |
678 |
672 |
679 |
673 *** System *** |
680 *** System *** |
674 |
681 |
675 * Global session timeout is multiplied by timeout_scale factor. This |
682 * Global session timeout is multiplied by timeout_scale factor. This |