--- a/src/HOLCF/Adm.thy Wed Nov 17 16:05:18 2010 -0800
+++ b/src/HOLCF/Adm.thy Wed Nov 17 16:13:33 2010 -0800
@@ -31,9 +31,9 @@
subsection {* Admissibility on chain-finite types *}
-text {* for chain-finite (easy) types every formula is admissible *}
+text {* For chain-finite (easy) types every formula is admissible. *}
-lemma adm_chfin: "adm (P::'a::chfin \<Rightarrow> bool)"
+lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)"
by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
subsection {* Admissibility of special formulae and propagation *}