# HG changeset patch
# User huffman
# Date 1290039213 28800
# Node ID dafba3a1dc5b4d65d98aaf424bf0a6538181a4c2
# Parent  e40e9e9769f4603a43d47e62a7850b57110f719e
declare adm_chfin [simp]

diff -r e40e9e9769f4 -r dafba3a1dc5b src/HOLCF/Adm.thy
--- 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 *}