| changeset 30661 | 54858c8ad226 |
| parent 30267 | 171b3bd93c90 |
| child 47380 | c4b2ec379fdd |
| 30660:53e1b1641f09 | 30661:54858c8ad226 |
|---|---|
1 (* Title: Glbs |
1 (* Author: Amine Chaieb, University of Cambridge *) |
2 Author: Amine Chaieb, University of Cambridge |
|
3 *) |
|
4 |
2 |
5 header{*Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs*} |
3 header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *} |
6 |
4 |
7 theory Glbs |
5 theory Glbs |
8 imports Lubs |
6 imports Lubs |
9 begin |
7 begin |
10 |
8 |