src/HOL/Real/Lubs.thy
changeset 15131 c69542757a4d
parent 14653 0848ab6fe5fc
child 15140 322485b816ac
equal deleted inserted replaced
15130:dc6be28d7f4e 15131:c69542757a4d
     4     Copyright   : 1998  University of Cambridge
     4     Copyright   : 1998  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 header{*Definitions of Upper Bounds and Least Upper Bounds*}
     7 header{*Definitions of Upper Bounds and Least Upper Bounds*}
     8 
     8 
     9 theory Lubs = Main:
     9 theory Lubs
       
    10 import Main
       
    11 begin
    10 
    12 
    11 text{*Thanks to suggestions by James Margetson*}
    13 text{*Thanks to suggestions by James Margetson*}
    12 
    14 
    13 constdefs
    15 constdefs
    14 
    16