src/HOL/HOLCF/Algebraic.thy
changeset 49834 b27bbb021df1
parent 41959 b460124855b8
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/Algebraic.thy	Fri Oct 12 15:08:29 2012 +0200
     1.2 +++ b/src/HOL/HOLCF/Algebraic.thy	Fri Oct 12 18:58:20 2012 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  subsection {* Type constructor for finite deflations *}
     1.6  
     1.7 -typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
     1.8 +typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
     1.9  by (fast intro: finite_deflation_bottom)
    1.10  
    1.11  instantiation fin_defl :: (bifinite) below
    1.12 @@ -74,7 +74,7 @@
    1.13  
    1.14  subsection {* Defining algebraic deflations by ideal completion *}
    1.15  
    1.16 -typedef (open) 'a defl = "{S::'a fin_defl set. below.ideal S}"
    1.17 +typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
    1.18  by (rule below.ex_ideal)
    1.19  
    1.20  instantiation defl :: (bifinite) below