--- a/src/HOL/HOL.thy Thu Apr 07 10:22:55 2005 +0200
+++ b/src/HOL/HOL.thy Thu Apr 07 13:29:41 2005 +0200
@@ -11,6 +11,28 @@
("~~/src/Provers/eqsubst.ML")
begin
+subsection {* Rules That Belong in Pure *}
+
+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 [CPure.elim_format]
+
+
subsection {* Primitive logic *}
subsubsection {* Core syntax *}