src/HOL/Conditionally_Complete_Lattices.thy
changeset 58889 5b7a9633cfa8
parent 57447 87429bdecad5
child 59452 2538b2c51769
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     2     Author:     Amine Chaieb and L C Paulson, University of Cambridge
     2     Author:     Amine Chaieb and L C Paulson, University of Cambridge
     3     Author:     Johannes Hölzl, TU München
     3     Author:     Johannes Hölzl, TU München
     4     Author:     Luke S. Serafin, Carnegie Mellon University
     4     Author:     Luke S. Serafin, Carnegie Mellon University
     5 *)
     5 *)
     6 
     6 
     7 header {* Conditionally-complete Lattices *}
     7 section {* Conditionally-complete Lattices *}
     8 
     8 
     9 theory Conditionally_Complete_Lattices
     9 theory Conditionally_Complete_Lattices
    10 imports Main
    10 imports Main
    11 begin
    11 begin
    12 
    12