# HG changeset patch
# User wenzelm
# Date 1114278579 -7200
# Node ID 222eeb9655f3ee6e35c82a0b9740ad9cc646dc9b
# Parent  d1001770af170bb0ff6ae9121576324065a72d90
tuned proofs;

diff -r d1001770af17 -r 222eeb9655f3 src/Pure/Pure.thy
--- 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]