src/HOL/Real/Lubs.thy
changeset 12671 bb6db6c0d4df
parent 9279 fb4186e20148
child 14368 2763da611ad9