src/HOL/Real/Lubs.thy
changeset 10017 e146bbfc38c1
parent 9279 fb4186e20148
child 14368 2763da611ad9
equal deleted inserted replaced
10016:3833b58a5d88 10017:e146bbfc38c1