# HG changeset patch
# User wenzelm
# Date 1026141847 -7200
# Node ID 685499c7321590aa384ed80debcf9fc32ef9da6c
# Parent  84b9de3cbc9177ced0394d71ceb528808de0e929
tuned;

diff -r 84b9de3cbc91 -r 685499c73215 src/ZF/Constructible/MetaExists.thy
--- a/src/ZF/Constructible/MetaExists.thy	Mon Jul 08 15:56:39 2002 +0200
+++ b/src/ZF/Constructible/MetaExists.thy	Mon Jul 08 17:24:07 2002 +0200
@@ -13,20 +13,15 @@
   "?? "        :: "[idts, o] => o"             ("(3\<Or>_./ _)" [0, 0] 0)
 
 lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
-proof -
+proof (unfold ex_def)
   assume P: "PROP P(x)"
-  show "?? x. PROP P(x)"
-  apply (unfold ex_def)
-  proof -
-    fix Q
-    assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
-    from P show "PROP Q" by (rule PQ)
-  qed
+  fix Q
+  assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q"
+  from P show "PROP Q" by (rule PQ)
 qed 
 
 lemma meta_exE: "[| ?? x. PROP P(x);  !!x. PROP P(x) ==> PROP R |] ==> PROP R"
-apply (unfold ex_def)
-proof -
+proof (unfold ex_def)
   assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
   assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
   from PR show "PROP R" by (rule QPQ)