tuned;

--- a/src/Pure/CPure.thy	Fri Oct 28 20:18:37 2005 +0200
+++ b/src/Pure/CPure.thy	Fri Oct 28 22:26:10 2005 +0200
@@ -1,6 +1,5 @@
 (*  Title:      Pure/CPure.thy
     ID:         $Id$
-    Author:     Makarius
 
 The CPure theory -- Pure with alternative application syntax.
 *)

--- a/src/Pure/Pure.thy	Fri Oct 28 20:18:37 2005 +0200
+++ b/src/Pure/Pure.thy	Fri Oct 28 22:26:10 2005 +0200
@@ -1,6 +1,5 @@
 (*  Title:      Pure/Pure.thy
     ID:         $Id$
-    Author:     Larry Paulson and Makarius
 
 The Pure theory.
 *)
@@ -12,18 +11,18 @@
 setup "Context.setup ()"
 
 
-text{*These meta-level elimination rules facilitate the use of assumptions
-that contain !! and ==>, especially in linear scripts. *}
+text{* These meta-level elimination rules facilitate the use of assumptions
+  that contain !! and ==>, especially in linear scripts. *}
 
 lemma meta_mp:
-  assumes major: "PROP P ==> PROP Q" and minor: "PROP P"
+  assumes "PROP P ==> PROP Q" and "PROP P"
   shows "PROP Q"
-    by (rule major [OF minor])
+    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
 
 lemma meta_spec:
-  assumes major: "!!x. PROP P(x)"
+  assumes "!!x. PROP P(x)"
   shows "PROP P(x)"
-    by (rule major)
+    by (rule `!!x. PROP P(x)`)
 
 lemmas meta_allE = meta_spec [elim_format]