changeset 40327 | 1dfdbd66093a |
parent 40321 | d065b195ec89 |
child 40436 | adb22dbb5242 |
--- a/src/HOLCF/LowerPD.thy Fri Oct 29 16:51:40 2010 -0700 +++ b/src/HOLCF/LowerPD.thy Fri Oct 29 17:15:28 2010 -0700 @@ -256,7 +256,7 @@ lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x" apply (safe elim!: compact_lower_unit) apply (simp only: compact_def lower_unit_below_iff [symmetric]) -apply (erule adm_subst [OF cont_Rep_CFun2]) +apply (erule adm_subst [OF cont_Rep_cfun2]) done lemma compact_lower_plus [simp]: