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 finite_lattice_complete < countable Class finite_lattice_complete is defined in Finite_Lattice but I have no idea why it should be a subclass of countable. Theory Finite_Lattice does not import Countable but Countable uses class finite. Is there some general potential problem with classes when merging theories? Thanks Tobias _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
