equal
deleted
inserted
replaced
676 profile_time (*CPU time*) |
676 profile_time (*CPU time*) |
677 profile_time_thread (*CPU time on this thread*) |
677 profile_time_thread (*CPU time on this thread*) |
678 profile_allocations (*overall heap allocations*) |
678 profile_allocations (*overall heap allocations*) |
679 |
679 |
680 * Antiquotation @{undefined} or \<^undefined> inlines (raise Match). |
680 * Antiquotation @{undefined} or \<^undefined> inlines (raise Match). |
|
681 |
|
682 * Antiquotation @{method NAME} inlines the (checked) name of the given |
|
683 Isar proof method. |
681 |
684 |
682 * Pretty printing of Poly/ML compiler output in Isabelle has been |
685 * Pretty printing of Poly/ML compiler output in Isabelle has been |
683 improved: proper treatment of break offsets and blocks with consistent |
686 improved: proper treatment of break offsets and blocks with consistent |
684 breaks. |
687 breaks. |
685 |
688 |