On 04/11/17 19:30, David Matthews wrote:
>
> I've had a look at this and pushed a change to IntInf.pow to Poly/ML
> master (c2a2961). It now uses Word.andb rather than IntInf.andb which
> avoids a call into the run-time system (RTS).
>
> However, this code hadn't changed since 5.6 and when I
On 03/11/2017 19:07, Makarius wrote:
On 03/11/17 19:26, Fabian Immler wrote:
I looked at it once more: profiling told me that IntInf.pow (in combination
with Par_List.map) seems to be the culprit.
The following snippet shows similar behavior:
ML ‹
fun powers [] = []
| powers (x::xs) =
Dear Makarius,
> *** Prover IDE -- Isabelle/Scala/jEdit ***
>
> * The command-line tool "isabelle jedit" provides more flexible options
> for session selection:
> - options -P opens the parent session image of -l
> - options -A and -B modify the meaning of -l to produce a base
> image on
See now http://isabelle.in.tum.de/repos/isabelle/rev/0230af0f3c59.
Florian
Am 19.10.2017 um 13:56 schrieb Florian Haftmann:
> Dear all,
>
> the nowadays ancient theory Nat_Transfer (essentially providing an
> attribute to transfer ad-hoc between theorems on nat vs. int) is almost
>
