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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev