# HG changeset patch
# User huffman
# Date 1269317514 25200
# Node ID 5ea16bc10a7a1856146b89ca04183a6f0baac1bb
# Parent  91a7311177c437f31b6bf3e015ecde7c5269fcda
remove admw predicate

diff -r 91a7311177c4 -r 5ea16bc10a7a src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Mon Mar 22 20:54:52 2010 -0700
+++ b/src/HOLCF/Fix.thy	Mon Mar 22 21:11:54 2010 -0700
@@ -261,29 +261,4 @@
   show "\<langle>?x, ?y\<rangle> \<sqsubseteq> z" using z 1 2 by simp
 qed
 
-subsection {* Weak admissibility *}
-
-definition
-  admw :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "admw P = (\<forall>F. (\<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)) \<longrightarrow> P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>))"
-
-text {* an admissible formula is also weak admissible *}
-
-lemma adm_impl_admw: "adm P \<Longrightarrow> admw P"
-apply (unfold admw_def)
-apply (intro strip)
-apply (erule admD)
-apply (rule chain_iterate)
-apply (erule spec)
-done
-
-text {* computational induction for weak admissible formulae *}
-
-lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
-by (simp add: fix_def2 admw_def)
-
-lemma def_wfix_ind:
-  "\<lbrakk>f \<equiv> fix\<cdot>F; admw P; \<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)\<rbrakk> \<Longrightarrow> P f"
-by (simp, rule wfix_ind)
-
 end