Re: [isabelle-dev] Unproven class relation finite_lattice_complete countable
On Sat, 29 Dec 2012, Florian Haftmann wrote: So far. I will stop for today, and I am not sure when I am able to turn back on the issue. But maybe I have found enough that the original authors can comment on it. Yet an even more minimal example I will study this a bit further ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Unproven class relation finite_lattice_complete countable
On Sat, 29 Dec 2012, Tobias Nipkow wrote: I have just added a new theory Library/Finite_Lattice. Just to make just well-defined: it refers to Isabelle/009a9fdabbad. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Unproven class relation finite_lattice_complete countable
Here something seems indeed to be wrong with the class edge completion in axclass.ML. I have attached a more minimal example and will investigate further. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de Countable.thy Description: application/extension-thy Finite_Lattice.thy Description: application/extension-thy Merge.thy Description: application/extension-thy signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Unproven class relation finite_lattice_complete countable
So far. I will stop for today, and I am not sure when I am able to turn back on the issue. But maybe I have found enough that the original authors can comment on it. Yet an even more minimal example Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de Base.thy Description: application/extension-thy Countable.thy Description: application/extension-thy Finite_Lattice.thy Description: application/extension-thy Merge.thy Description: application/extension-thy signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
