# HG changeset patch
# User nipkow
# Date 1182319796 -7200
# Node ID cec811764a388cd6908ff401d88b8d4af263a060
# Parent  25ca91279a9b65a4aa8696da5806d79e81b08915
added meta_impE

diff -r 25ca91279a9b -r cec811764a38 src/Pure/Pure.thy
--- 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)"