src/Pure/Isar/isar_thy.ML

 Pure/Isar derived theory operations.
 *)
 
 signature ISAR_THY =
 sig
+  val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_text: Comment.text -> theory -> theory
   val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
   val add_chapter: Comment.text -> theory -> theory
   val add_section: Comment.text -> theory -> theory
   val add_subsection: Comment.text -> theory -> theory

 
 (** derived theory and proof operations **)
 
 (* formal comments *)
 
+fun add_txt comment prf = prf;
 fun add_text comment thy = thy;
 fun add_title title author date thy = thy;
 val add_chapter = add_text;
 val add_section = add_text;
 val add_subsection = add_text;