# HG changeset patch
# User paulson
# Date 1112873381 -7200
# Node ID 042692b6275d6eca4249f752b3ae7762d1737eff
# Parent  ce00c47dd100bd002e44e0a1d3f68d9e245021ba
new meta-level rules

diff -r ce00c47dd100 -r 042692b6275d src/HOL/HOL.thy
--- 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 *}