[isabelle-dev] Unproven class relation finite_lattice_complete < countable
Tobias Nipkow
nipkow at in.tum.de
Sat Dec 29 17:36:28 CET 2012
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
More information about the isabelle-dev
mailing list