tuned proofs;

--- a/src/Pure/Pure.thy	Sat Apr 23 19:49:26 2005 +0200
+++ b/src/Pure/Pure.thy	Sat Apr 23 19:49:39 2005 +0200
@@ -18,16 +18,12 @@
 lemma meta_mp:
   assumes major: "PROP P ==> PROP Q" and minor: "PROP P"
   shows "PROP Q"
-proof -
-  show "PROP Q" by (rule major [OF minor])
-qed
+    by (rule major [OF minor])
 
 lemma meta_spec:
   assumes major: "!!x. PROP P(x)"
   shows "PROP P(x)"
-proof -
-  show "PROP P(x)" by (rule major)
-qed
+    by (rule major)
 
 lemmas meta_allE = meta_spec [elim_format]