src/Pure/Pure.thy
changeset 62944 3ee643c5ed00
parent 62913 13252110a6fe
child 62969 9f394a16c557
     1.1 --- a/src/Pure/Pure.thy	Sun Apr 10 21:30:48 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Sun Apr 10 21:46:12 2016 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/Pure.thy
     1.5      Author:     Makarius
     1.6  
     1.7 -Final stage of bootstrapping Pure, based on implicit background theory.
     1.8 +The Pure theory, with definitions of Isar commands and some lemmas.
     1.9  *)
    1.10  
    1.11  theory Pure
    1.12 @@ -1282,7 +1282,7 @@
    1.13  in end\<close>
    1.14  
    1.15  
    1.16 -section \<open>Further content for the Pure theory\<close>
    1.17 +section \<open>Auxiliary lemmas\<close>
    1.18  
    1.19  subsection \<open>Meta-level connectives in assumptions\<close>
    1.20