src/HOL/Library/Lattice_Constructions.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Lattice_Constructions.thy	Thu Sep 11 19:26:59 2014 +0200
     1.2 +++ b/src/HOL/Library/Lattice_Constructions.thy	Thu Sep 11 19:32:36 2014 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  subsection {* Values extended by a bottom element *}
     1.6  
     1.7 -datatype_new 'a bot = Value 'a | Bot
     1.8 +datatype 'a bot = Value 'a | Bot
     1.9  
    1.10  instantiation bot :: (preorder) preorder
    1.11  begin
    1.12 @@ -108,7 +108,7 @@
    1.13  
    1.14  section {* Values extended by a top element *}
    1.15  
    1.16 -datatype_new 'a top = Value 'a | Top
    1.17 +datatype 'a top = Value 'a | Top
    1.18  
    1.19  instantiation top :: (preorder) preorder
    1.20  begin
    1.21 @@ -207,7 +207,7 @@
    1.22  
    1.23  subsection {* Values extended by a top and a bottom element *}
    1.24  
    1.25 -datatype_new 'a flat_complete_lattice = Value 'a | Bot | Top
    1.26 +datatype 'a flat_complete_lattice = Value 'a | Bot | Top
    1.27  
    1.28  instantiation flat_complete_lattice :: (type) order
    1.29  begin