It’s nice that global theories don’t have to be qualified. But it’s a bit
strange that it's forbidden to qualify them.
--lcp
> On 2 Nov 2017, at 17:21, Makarius wrote:
>
>> On 02/11/17 17:47, Lawrence Paulson wrote:
>>
>> And I have triple checked that Probability is spelt correctly. Any hint
On 02/11/17 17:47, Lawrence Paulson wrote:
> And I have triple checked that Probability is spelt correctly. Any hints?
Since Isabelle/f27488f47a47 you can use completion there (on the theory
base name).
E.g. "ALi" completes "HOL-Library.AList".
Makarius
On 02/11/17 16:11, Lars Hupel wrote:
>
> Tobias and me have discovered an interesting discrepancy between your
> AFP slow setup and our AFP slow setup. They run on identical hardware
> with the only difference of 6 vs 8 threads. On 6 threads, it runs
> significantly faster. For example, Flyspeck-T
Hi Larry,
in ~~/src/HOL/ROOT, the theory Probability is declared as "global". That means
that you must import it without any session qualification (just like Main or
Complex_Main).
Dmitriy
> On 2 Nov 2017, at 17:47, Lawrence Paulson wrote:
>
> I’ve been converting some theories from the old
I’ve been converting some theories from the old pathname syntax to the new
setup. I have the line
imports "HOL-Probability.Probability”
but it is rejected with the message
Bad theory import "HOL-Probability.Probability"
If instead I import "HOL-Probability.Random_Permutations”
> We are presently testing Poly/ML 5.7.1 by default (see
> Isabelle/aefaaef29c58) and there are already interesting performance
> figures, e.g. see:
>
> http://isabelle.in.tum.de/devel/build_status
> http://isabelle.in.tum.de/devel/build_status/Linux_A
> http://isabelle.in.tum.de/devel/build_statu
I should have sent the message below also to isabelle-dev, sorry about that.
Has anything changed about integers in Poly/ML 5.7.1?
Lorenz_C0 did slow down by a factor of 5, which I find quite extreme.
Best,
Fabian
> Am 28.10.2017 um 23:57 schrieb Fabian Immler :
>
> Lorenz_C0 is one of those "m
On 28/10/17 22:26, Makarius wrote:
>
> I still have some ideas for "isabelle build" in the pipeline (for
> several years) to skip building intermediate heaps in the first place.
> Then AFP (without the "slow" sessions) could shrink to 50% .. 20% build
> time.
>
> Until that emerges, AFP contributo
*** 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 the spot, based on the specifi
