src/ZF/Constructible/MetaExists.thy
changeset 13315 685499c73215
parent 13314 84b9de3cbc91
child 13505 52a16cb7fefb
     1.1 --- a/src/ZF/Constructible/MetaExists.thy	Mon Jul 08 15:56:39 2002 +0200
     1.2 +++ b/src/ZF/Constructible/MetaExists.thy	Mon Jul 08 17:24:07 2002 +0200
     1.3 @@ -13,20 +13,15 @@
     1.4    "?? "        :: "[idts, o] => o"             ("(3\<Or>_./ _)" [0, 0] 0)
     1.5  
     1.6  lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
     1.7 -proof -
     1.8 +proof (unfold ex_def)
     1.9    assume P: "PROP P(x)"
    1.10 -  show "?? x. PROP P(x)"
    1.11 -  apply (unfold ex_def)
    1.12 -  proof -
    1.13 -    fix Q
    1.14 -    assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
    1.15 -    from P show "PROP Q" by (rule PQ)
    1.16 -  qed
    1.17 +  fix Q
    1.18 +  assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
    1.19 +  from P show "PROP Q" by (rule PQ)
    1.20  qed 
    1.21  
    1.22  lemma meta_exE: "[| ?? x. PROP P(x);  !!x. PROP P(x) ==> PROP R |] ==> PROP R"
    1.23 -apply (unfold ex_def)
    1.24 -proof -
    1.25 +proof (unfold ex_def)
    1.26    assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
    1.27    assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
    1.28    from PR show "PROP R" by (rule QPQ)