--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy Tue Oct 09 17:33:46 2012 +0200
@@ -80,13 +80,13 @@
text {* Use @{text pcpodef} with the appropriate type combinator. *}
-pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
+pcpodef 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
+pcpodef 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
-pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
+pcpodef 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}