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

Gerwin Klein gerwin.klein at nicta.com.au
Fri Sep 9 01:19:14 CEST 2011

>> 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.


More information about the isabelle-dev mailing list