[isabelle-dev] Unproven class relation finite_lattice_complete countable

I have just added a new theory Library/Finite_Lattice. It clashes with theory Library/Countable in a way I don't understand. If you import both theory Scratch imports ~~/src/HOL/Library/Finite_Lattice ~~/src/HOL/Library/Countable begin Isabelle complains Unproven class relation

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

Re: [isabelle-dev] Proposing extensions to the Isabelle library?

On Fri, 28 Dec 2012, Christian Sternagel wrote: the necessary steps are outlined in the community wiki, here https://isabelle.in.tum.de/community/Publish_contributions_as_an_external Since the status of the wiki is not clear at the moment. The status of the wiki is unclear for 1 year. I

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

[isabelle-dev] Graph_Display.graphview_reportN resp. subtractive change of print mode

The graphview plugin, despite significant progress in the past weeks esp. wrt. performance, is IMHO still not suitable to manage our typical graphs (in particular class_deps), mainly due to too small-sized nodes resp. too wide distances. Unfortunately, the print mode

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: