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