[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
makarius at sketis.net
Thu Sep 8 23:13:52 CEST 2011
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.
More information about the isabelle-dev