# HG changeset patch
# User wenzelm
# Date 1114113960 -7200
# Node ID 42c75e0c9140ac06ae1b4c774b30b0dcd1a0d175
# Parent  fda379c17260a1009b4d4a08b3c272f0ed6f78cc
The Pure theory.

diff -r fda379c17260 -r 42c75e0c9140 src/Pure/Pure.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Pure.thy	Thu Apr 21 22:06:00 2005 +0200
@@ -0,0 +1,34 @@
+(*  Title:      Pure/Pure.thy
+    ID:         $Id$
+    Author:     Larry Paulson and Makarius
+
+The Pure theory.
+*)
+
+theory Pure
+imports ProtoPure
+begin
+
+setup "Context.setup ()"
+
+
+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"
+  shows "PROP Q"
+proof -
+  show "PROP Q" by (rule major [OF minor])
+qed
+
+lemma meta_spec:
+  assumes major: "!!x. PROP P(x)"
+  shows "PROP P(x)"
+proof -
+  show "PROP P(x)" by (rule major)
+qed
+
+lemmas meta_allE = meta_spec [elim_format]
+
+end