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

[Lawrence Paulson]

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 ex/Set_Theory.thy, there is a non-terminating »force« proof, which is
> a little bit worrying since I guess that one worked in Isabelle2007.
> Maybe someone can inspect the history on that?

If my memory is correct, this one worked in a reasonable amount of time on hardware of the late 1990s. But it isn't that surprising that later changes could interfere with its functioning when we restore the set type. I see that it does work with auto, but it's slow, thirty seconds or more.

Larry

On 25 Aug 2011, at 21:45, Florian Haftmann wrote:

> I think it is best to leave the AFP aside for the moment and figure out
> still existing problems in the distribution.  According to my knowledge,
> the following session produce problems:
> 
> HOL-ex FAILED
> HOL-Hoare_Parallel FAILED
> HOL-Nominal FAILED
> HOL-Library FAILED
> HOL-Metis_Examples FAILED
> HOL-MicroJava FAILED
> HOL-Nitpick_Examples FAILED
> HOL-Quotient_Examples FAILED
> HOL-Predicate_Compile_Examples FAILED
> HOL-Word-SMT_Examples FAILED
> HOL-TPTP FAILED
> HOL-Probability FAILED