src/HOL/HOLCF/ex/Domain_Proofs.thy
changeset 49759 ecf1d5d87e5e
parent 44066 d74182c93f04
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Oct 09 16:58:36 2012 +0200
     1.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Oct 09 17:33:46 2012 +0200
     1.3 @@ -80,13 +80,13 @@
     1.4  
     1.5  text {* Use @{text pcpodef} with the appropriate type combinator. *}
     1.6  
     1.7 -pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
     1.8 +pcpodef 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
     1.9  by (rule defl_set_bottom, rule adm_defl_set)
    1.10  
    1.11 -pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
    1.12 +pcpodef 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
    1.13  by (rule defl_set_bottom, rule adm_defl_set)
    1.14  
    1.15 -pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
    1.16 +pcpodef 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
    1.17  by (rule defl_set_bottom, rule adm_defl_set)
    1.18  
    1.19  text {* Prove rep instance using lemma @{text typedef_rep_class}. *}