src/HOL/Lubs.thy
changeset 30681 27ee3f4ea99c
parent 29654 24e73987bfe2
child 30738 0842e906300c