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

[Gerwin Klein]

On 11/08/2011, at 2:44 PM, Florian Haftmann wrote:

> Then the following sessions fail:
>  HOL-Algebra
>  HOL-Auth
>  HOLCF
>  HOL-ex
>  HOL-Hahn_Banach
>  HOL-Hoare_Parallel
>  HOL-IMP
>  HOL-Imperative_HOL
>  HOL-Induct
>  HOL-Library
>  HOL-Matrix
>  HOL-Metis_Examples
>  HOL-MicroJava
>  HOL-Multivariate_Analysis
>  HOL-Nitpick_Examples
>  HOL-Nominal
>  HOL-NSA
>  HOL-Old_Number_Theory
>  HOL-Predicate_Compile_Examples
>  HOL-Quotient_Examples
>  HOL-TPTP
>  HOL-UNITY
>  HOL-Word-SMT_Examples

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.

Gerwin