--- a/src/Pure/Pure.thy Wed Jun 20 05:18:39 2007 +0200
+++ b/src/Pure/Pure.thy Wed Jun 20 08:09:56 2007 +0200
@@ -18,6 +18,8 @@
shows "PROP Q"
by (rule `PROP P ==> PROP Q` [OF `PROP P`])
+lemmas meta_impE = meta_mp [elim_format]
+
lemma meta_spec:
assumes "!!x. PROP P(x)"
shows "PROP P(x)"