# HG changeset patch
# User huffman
# Date 1127408765 -7200
# Node ID f12d7ac88eb4a128a034c48c55f6dda91e167873
# Parent  6eab0f1cb0fe705a07edc50888a984d7046e63eb
cleaned up

diff -r 6eab0f1cb0fe -r f12d7ac88eb4 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Thu Sep 22 18:59:41 2005 +0200
+++ b/src/HOLCF/Fix.thy	Thu Sep 22 19:06:05 2005 +0200
@@ -228,7 +228,7 @@
 
 text {* computational induction for weak admissible formulae *}
 
-lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n F UU)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
+lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n F \<bottom>)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
 by (simp add: fix_def2 admw_def)
 
 lemma def_wfix_ind:
diff -r 6eab0f1cb0fe -r f12d7ac88eb4 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Thu Sep 22 18:59:41 2005 +0200
+++ b/src/HOLCF/Up.thy	Thu Sep 22 19:06:05 2005 +0200
@@ -130,9 +130,7 @@
 apply (simp add: expand_fun_eq)
 apply (erule exE, rename_tac j)
 apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
-apply (rule conjI)
 apply (simp add: up_lemma4)
-apply (rule conjI)
 apply (simp add: up_lemma6 [THEN thelubI])
 apply (rule_tac x=j in exI)
 apply (simp add: up_lemma3)
@@ -143,8 +141,7 @@
 apply (rule_tac x="Iup (lub (range A))" in exI)
 apply (erule_tac j1="j" in is_lub_range_shift [THEN iffD1])
 apply (simp add: is_lub_Iup thelubE)
-apply (rule_tac x="Ibottom" in exI)
-apply (rule lub_const)
+apply (rule exI, rule lub_const)
 done
 
 instance u :: (cpo) cpo
@@ -152,7 +149,7 @@
 
 subsection {* Type @{typ "'a u"} is pointed *}
 
-lemma least_up: "EX x::'a u. ALL y. x\<sqsubseteq>y"
+lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
 apply (rule_tac x = "Ibottom" in exI)
 apply (rule minimal_up [THEN allI])
 done