src/Pure/Isar/isar_thy.ML

 *)
 
 signature ISAR_THY =
 sig
   val add_text: string -> theory -> theory
+  val add_title: string -> string -> string -> theory -> theory
   val add_chapter: string -> theory -> theory
   val add_section: string -> theory -> theory
   val add_subsection: string -> theory -> theory
   val add_subsubsection: string -> theory -> theory
   val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory

 (** derived theory and proof operations **)
 
 (* formal comments *)	(* FIXME dummy *)
 
 fun add_text (txt:string) (thy:theory) = thy;
+fun add_title title author date thy = thy;
 val add_chapter = add_text;
 val add_section = add_text;
 val add_subsection = add_text;
 val add_subsubsection = add_text;