src/HOL/Real/Lubs.thy
changeset 8970 3ac901561f33
parent 7562 8519d5019309
child 9279 fb4186e20148
equal deleted inserted replaced
8969:23c6e0ca0086 8970:3ac901561f33