src/HOL/Set_Interval.thy
changeset 58889 5b7a9633cfa8
parent 57514 bdc2c6b40bf2
child 58970 2f65dcd32a59
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     9 describe the lower and upper bound and x,y : {c,o,i}
     9 describe the lower and upper bound and x,y : {c,o,i}
    10 where c = closed, o = open, i = infinite.
    10 where c = closed, o = open, i = infinite.
    11 Examples: Ico = {_ ..< _} and Ici = {_ ..}
    11 Examples: Ico = {_ ..< _} and Ici = {_ ..}
    12 *)
    12 *)
    13 
    13 
    14 header {* Set intervals *}
    14 section {* Set intervals *}
    15 
    15 
    16 theory Set_Interval
    16 theory Set_Interval
    17 imports Lattices_Big Nat_Transfer
    17 imports Lattices_Big Nat_Transfer
    18 begin
    18 begin
    19 
    19