changed two goals formulated with 8bit font
authoroheimb
Wed, 24 Apr 1996 13:01:13 +0200
changeset 1681 d9aaae4ff6c3
parent 1680 d0d607937aa0
child 1682 dd1ced7f1ff1
changed two goals formulated with 8bit font
src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Wed Apr 24 11:20:57 1996 +0200
+++ b/src/HOLCF/Fix.ML	Wed Apr 24 13:01:13 1996 +0200
@@ -1177,10 +1177,10 @@
 
 
 qed_goal "adm_not_conj"  Fix.thy  
- " adm (x.  P x); adm (x.  Q x)   adm (x.  (P x  Q x))" (fn prems =>[
+"[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"(fn prems=>[
 	cut_facts_tac prems 1,
 	subgoal_tac 
-	"(x.  (P x  Q x)) = (x.  P x   Q x)" 1,
+	"(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1,
 	rtac ext 2,
 	fast_tac HOL_cs 2,
 	etac ssubst 1,
@@ -1188,8 +1188,8 @@
 	atac 1]);
 
 qed_goalw "admI" Fix.thy [adm_def]
- "(Y.  is_chain Y ; i. P(Y i) ; i. j. i < j  Y i  Y j  Y i  Y j   \
-\ P(lub (range Y)))  adm P" 
+ "(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
+\ ==> P(lub (range Y))) ==> adm P" 
  (fn prems => [
 	strip_tac 1,
 	case_tac "finite_chain Y" 1,