src/HOL/HOLCF/Domain.thy
changeset 40834 a1249aeff5b6
parent 40830 158d18502378
child 41285 efd23c1d9886
     1.1 --- a/src/HOL/HOLCF/Domain.thy	Tue Nov 30 15:34:51 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Domain.thy	Tue Nov 30 15:56:19 2010 -0800
     1.3 @@ -113,7 +113,7 @@
     1.4    have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
     1.5      unfolding emb
     1.6      apply (rule beta_cfun)
     1.7 -    apply (rule typedef_cont_Rep [OF type below adm_defl_set])
     1.8 +    apply (rule typedef_cont_Rep [OF type below adm_defl_set cont_id])
     1.9      done
    1.10    have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
    1.11      unfolding prj