src/Pure/Pure.thy
changeset 18710 527aa560a9e0
parent 18663 8474756e4cbf
child 18836 3a1e4ee72075
     1.1 --- a/src/Pure/Pure.thy	Thu Jan 19 21:22:14 2006 +0100
     1.2 +++ b/src/Pure/Pure.thy	Thu Jan 19 21:22:15 2006 +0100
     1.3 @@ -1,5 +1,7 @@
     1.4  (*  Title:      Pure/Pure.thy
     1.5      ID:         $Id$
     1.6 +
     1.7 +The actual Pure theory.
     1.8  *)
     1.9  
    1.10  header {* The Pure theory *}
    1.11 @@ -8,8 +10,11 @@
    1.12  imports ProtoPure
    1.13  begin
    1.14  
    1.15 +subsection {* Common setup of internal components *}
    1.16 +
    1.17  setup
    1.18  
    1.19 +
    1.20  subsection {* Meta-level connectives in assumptions *}
    1.21  
    1.22  lemma meta_mp: