src/Pure/Isar/isar_thy.ML

   val add_chapter: Comment.text -> theory -> theory
   val add_section: Comment.text -> theory -> theory
   val add_subsection: Comment.text -> theory -> theory
   val add_subsubsection: Comment.text -> theory -> theory
   val add_text: Comment.text -> theory -> theory
+  val add_verbatim: Comment.text -> theory -> theory
   val add_sect: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_subsect: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
+  val add_verb: Comment.text -> ProofHistory.T -> ProofHistory.T
   val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory
   val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
   val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
   val add_classrel_i: (class * class) * Comment.text -> theory -> theory
   val add_defsort: xsort * Comment.text -> theory -> theory

 
 fun add_header comment =
   Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF);
 
 fun add_text comment thy = thy:theory;
+val add_verbatim = add_text;
 val add_chapter = add_text;
 
 fun gen_add_section add present txt thy =
   (Context.setmp (Some thy) present (Comment.string_of txt); add txt thy);
 
 val add_section = gen_add_section add_text Present.section;
 val add_subsection = gen_add_section add_text Present.subsection;
 val add_subsubsection = gen_add_section add_text Present.subsubsection;
 
 fun add_txt comment = ProofHistory.apply Proof.assert_forward;
+val add_verb = add_txt;
 val add_sect = add_txt;
 val add_subsect = add_txt;
 val add_subsubsect = add_txt;