--- a/src/Pure/Pure.thy Tue Sep 19 23:15:35 2006 +0200 +++ b/src/Pure/Pure.thy Tue Sep 19 23:15:36 2006 +0200 @@ -10,6 +10,7 @@ setup -- {* Common setup of internal components *} + subsection {* Meta-level connectives in assumptions *} lemma meta_mp: