Am 21.02.2014 um 20:13 schrieb Florian Haftmann
:
>> *** Prover failed: error submitting job
>> *** At command "by" (line 28 of
>> "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
>> Unfinished session(s): HOL-Library
>> 0:07:48 elapsed time, 0:19:43 cpu time, factor 2.52
>
> Three weeks ago a r
Referring to isabelle hg id eb07b0acbebc:
> haftmann@lxbroy10:~/data/isabelle/master$ ISABELLE_FULL_TEST=true isabelle
> build HOL-Library
> Running HOL-Library ...
>
> HOL-Library FAILED
> (see also
> /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.1_x86-linux/log/HOL-Library)
>
> **
* Improved completion based on context information about embedded
languages: keywords are only completed for outer syntax, symbols for
languages that support them. E.g. no symbol completion for ML source,
but within ML strings, comments, antiquotations.
This refers to Isabelle/5ff4742f27ec. No
Hi,
I'm aware of a number of assertion failures that seem to occur
intermittently. This is one of the ones on my list. I suspect they are
all symptoms of the same bug but I have never been able to narrow it
down or reproduce it. It does seem to occur when the memory management
is under heav
Hi Josh,
Am 21.02.2014 um 07:12 schrieb Josh Tilles :
> Sure! There are some mathematical topics that I’d like to use Isabelle to
> study, but those topics require an intuitionistic setting. (the primary
> example is infinitesimal analysis) Also, the way that
> `src/HOL/ex/Higher_Order_Logic.t
