author | wenzelm |
Thu, 19 Jan 2006 21:22:15 +0100 | |
changeset 18710 | 527aa560a9e0 |
parent 18709 | f174ebc26073 |
child 18711 | cf020c54e2f5 |
src/Pure/Pure.thy | file | annotate | diff | comparison | revisions |
--- a/src/Pure/Pure.thy Thu Jan 19 21:22:14 2006 +0100 +++ b/src/Pure/Pure.thy Thu Jan 19 21:22:15 2006 +0100 @@ -1,5 +1,7 @@ (* Title: Pure/Pure.thy ID: $Id$ + +The actual Pure theory. *) header {* The Pure theory *} @@ -8,8 +10,11 @@ imports ProtoPure begin +subsection {* Common setup of internal components *} + setup + subsection {* Meta-level connectives in assumptions *} lemma meta_mp: