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

[Gerwin Klein]

>> 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 looks very nice btw! Exactly what I need to do demos in the lecture with my old 2 core/2GB MacBook Air.

I'm happy to look at MicroJava in a while. The last time I checked it failed because of something in HOL/Library (CSet? not sure any more). Almost all of it was written before the set/predicate unification, so there shouldn't be anything fundamental.

Cheers,
Gerwin