# HG changeset patch
# User wenzelm
# Date 921185630 -3600
# Node ID a4c75cbd2fbfcd0577dea06ac45cb0013fa1b22e
# Parent  5a76eb9030df187f2948955127a31d8c881e696a
add_title;

diff -r 5a76eb9030df -r a4c75cbd2fbf src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Mar 11 21:53:36 1999 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Thu Mar 11 21:53:50 1999 +0100
@@ -13,6 +13,7 @@
 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
@@ -74,6 +75,7 @@
 (* 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;