# HG changeset patch
# User wenzelm
# Date 1137702135 -3600
# Node ID 527aa560a9e0412b880cb7c8ac284814326be71a
# Parent  f174ebc26073fe90e44070882e0da9882c6a95e3
tuned comments;

diff -r f174ebc26073 -r 527aa560a9e0 src/Pure/Pure.thy
--- 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: