The AFP test has been failing for random entries with segmentation fault
over the last few days. Now the same thing is happening when I test HOL
locally on my Mac. My latest test run yielded
Running HOL-IMPP ...
/Users/nipkow/isabelle/lib/scripts/run-polyml-5.5.2: line 82: 473 Segmentation
fau
Just a reminder that this old thread is not yet resolved and currently
I'm essentially stuck.
Independent of my being stuck, could one of the devs apply at least the
first of the following attached patches (and the second one depending on
whether dropping semicolons is in general seen as good
Here is a related thread
https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04950.html
which was originated by myself ;) (how embarassing).
cheers
chris
On 01/16/2015 02:35 PM, Christian Sternagel wrote:
Dear all,
in Isabelle2014 as well as c7f6f01ede15 I notic
Dear all,
in Isabelle2014 as well as c7f6f01ede15 I noticed that the output when
using adhoc overloading together with abbreviations is not optimal
(maybe this was already discovered before but I forgot about it). Now,
it turns out that the same issue (at least superficially it's the same,
bu
As of c7f6f01ede15 I noticed the following behavior. Suppose I have a
theory file with the following content
theory Foo
imports
Main
begin
end
So far so good. Now I add another import.
theory Foo
imports
Main
"~~/src/HOL/Tools/Adhoc_Overloading"
begin
end
By accide
On 15.01.2015 15:59, Makarius wrote:
> On Tue, 13 Jan 2015, Lars Noschinski wrote:
>
>> in Isabelle 2014, on can enter \<^sub> and \<^sup> via C+e DOWN and C+e
>> UP, respectively. In 91649ea1b32c, these shortcuts don't work anymore
>> (at least for me).
>
> This should still work. Can you try it
