| changeset 40327 | 1dfdbd66093a |
| parent 40038 | 9d061b3d8f46 |
| child 40502 | 8e92772bc0e8 |
--- a/src/HOLCF/Algebraic.thy Fri Oct 29 16:51:40 2010 -0700 +++ b/src/HOLCF/Algebraic.thy Fri Oct 29 17:15:28 2010 -0700 @@ -191,7 +191,7 @@ lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d" apply (rule iffI) apply (simp only: compact_def cast_below_cast [symmetric]) -apply (erule adm_subst [OF cont_Rep_CFun2]) +apply (erule adm_subst [OF cont_Rep_cfun2]) apply (erule compact_cast) done