src/Pure/Isar/isar_thy.ML
changeset 7172 9ecd66cf546d
parent 7103 1c44df10a7bc
child 7176 a329a37ed91a
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Aug 03 19:04:02 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Aug 03 19:04:20 1999 +0200
     1.3 @@ -7,13 +7,16 @@
     1.4  
     1.5  signature ISAR_THY =
     1.6  sig
     1.7 -  val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
     1.8 -  val add_text: Comment.text -> theory -> theory
     1.9    val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
    1.10    val add_chapter: Comment.text -> theory -> theory
    1.11    val add_section: Comment.text -> theory -> theory
    1.12    val add_subsection: Comment.text -> theory -> theory
    1.13    val add_subsubsection: Comment.text -> theory -> theory
    1.14 +  val add_text: Comment.text -> theory -> theory
    1.15 +  val add_sect: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.16 +  val add_subsect: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.17 +  val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.18 +  val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.19    val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
    1.20    val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
    1.21    val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
    1.22 @@ -157,7 +160,6 @@
    1.23  
    1.24  (* formal comments *)
    1.25  
    1.26 -fun add_txt comment = ProofHistory.apply Proof.assert_forward;
    1.27  fun add_text comment thy = thy;
    1.28  fun add_title title author date thy = thy;
    1.29  val add_chapter = add_text;
    1.30 @@ -165,6 +167,11 @@
    1.31  val add_subsection = add_text;
    1.32  val add_subsubsection = add_text;
    1.33  
    1.34 +fun add_txt comment = ProofHistory.apply Proof.assert_forward;
    1.35 +val add_sect = add_text;
    1.36 +val add_subsect = add_text;
    1.37 +val add_subsubsect = add_text;
    1.38 +
    1.39  
    1.40  (* signature and syntax *)
    1.41