src/HOLCF/Cprod.thy
changeset 25907 695a9d88d697
parent 25906 2179c6661218
child 25908 d8ce142f7e6e
     1.1 --- a/src/HOLCF/Cprod.thy	Mon Jan 14 20:28:59 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Mon Jan 14 20:35:52 2008 +0100
     1.3 @@ -15,17 +15,16 @@
     1.4  
     1.5  subsection {* Type @{typ unit} is a pcpo *}
     1.6  
     1.7 -instantiation unit :: sq_ord
     1.8 +instantiation unit :: po
     1.9  begin
    1.10  
    1.11  definition
    1.12    less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
    1.13  
    1.14 -instance ..
    1.15 -end
    1.16 +instance
    1.17 +by intro_classes simp_all
    1.18  
    1.19 -instance unit :: po
    1.20 -by intro_classes simp_all
    1.21 +end
    1.22  
    1.23  instance unit :: finite_po ..
    1.24