src/HOL/Lattices_Big.thy
changeset 78130 8234c42d20e6
parent 75669 43f5dfb7fa35
child 80175 200107cdd3ac