tuned comments;
authorwenzelm
Thu Jan 19 21:22:15 2006 +0100 (2006-01-19 ago)
changeset 18710527aa560a9e0
parent 18709 f174ebc26073
child 18711 cf020c54e2f5
tuned comments;
src/Pure/Pure.thy
     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: