src/HOL/Algebra/Lattice.thy
changeset 29285 5cf577cb2253
parent 29242 e190bc2a5399
child 30363 9b8d9b6ef803