added meta_impE

--- 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)"