src/HOL/Algebra/Lattice.thy
changeset 16417 9bc16273c2d4
parent 16325 a6431098a929
child 19286 83404ccd270a
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     5   Copyright: Clemens Ballarin
     5   Copyright: Clemens Ballarin
     6 *)
     6 *)
     7 
     7 
     8 header {* Orders and Lattices *}
     8 header {* Orders and Lattices *}
     9 
     9 
    10 theory Lattice = Main:
    10 theory Lattice imports Main begin
    11 
    11 
    12 text {* Object with a carrier set. *}
    12 text {* Object with a carrier set. *}
    13 
    13 
    14 record 'a partial_object =
    14 record 'a partial_object =
    15   carrier :: "'a set"
    15   carrier :: "'a set"