On Fri, 26 Aug 2011, Lawrence Paulson wrote:
I took a look at some of these. HOL-Library fails in your own Cset.thy,
where presumably you know what you are doing (particularly as this
theory involves execution I should stay away from it). Similarly I'm not
sure I'm the right person to fix HOL-Nominal or HOL-MicroJava. PG is
very fragile just now, which makes working very tiresome.
In the past few days I have managed to overcome some serious performance
bottle necks in Isabelle/jEdit (cf. changes leading up to 03a5ba7213cf
from Tuesday this week).
This means one can now load full sessions like MicroJava into the Prover
IDE, even on a two-core machine (say with 4 GB, but it also works with 2
GB to some extent). Minor omission: I still need to make the crude "Prover
Session / Theory Status" overview panel more comprehensive.
So maintainance of old theory collections could become eanjoyable again,
after unlearning some Escape-Meta-Alt-Control-Shift key sequences.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
