[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
gerwin.klein at nicta.com.au
Sat Aug 13 12:22:05 CEST 2011
On 11/08/2011, at 2:44 PM, Florian Haftmann wrote:
> Then the following sessions fail:
Some more data from HOL-IMP and HOL-MicroJava: the former was trivial to fix (patch in main repository already). MJ after removing an unused lemma only seems to require a working Library/More_Set.thy to get through (haven't done anything about that one).
At least for applications in that style, I don't think we need to expect much pain for going back to a separate set type.
More information about the isabelle-dev