[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Makarius]

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