src/HOL/Real/Lubs.ML
changeset 5253 82a5ca6290aa
parent 5148 74919e8f221c
child 7219 4e3f386c2e37