# HG changeset patch
# User wenzelm
# Date 1130531170 -7200
# Node ID d1ff9ebb8bcb59423f1f42fd55476330bbfcd52e
# Parent  82206a6c75c0d510995a3d204806e1d9c8dc8cf0
tuned;

diff -r 82206a6c75c0 -r d1ff9ebb8bcb src/Pure/CPure.thy
--- 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.
 *)
diff -r 82206a6c75c0 -r d1ff9ebb8bcb src/Pure/Pure.thy
--- 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]