Comment.text;
authorwenzelm
Fri Apr 30 18:06:49 1999 +0200 (1999-04-30 ago)
changeset 655228553eba1913
parent 6551 de4047b03017
child 6553 dc962d157a63
Comment.text;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Apr 30 18:06:35 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 30 18:06:49 1999 +0200
     1.3 @@ -11,12 +11,12 @@
     1.4  
     1.5  signature ISAR_THY =
     1.6  sig
     1.7 -  val add_text: string -> theory -> theory
     1.8 -  val add_title: string -> string -> string -> theory -> theory
     1.9 -  val add_chapter: string -> theory -> theory
    1.10 -  val add_section: string -> theory -> theory
    1.11 -  val add_subsection: string -> theory -> theory
    1.12 -  val add_subsubsection: string -> theory -> theory
    1.13 +  val add_text: Comment.text -> theory -> theory
    1.14 +  val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
    1.15 +  val add_chapter: Comment.text -> theory -> theory
    1.16 +  val add_section: Comment.text -> theory -> theory
    1.17 +  val add_subsection: Comment.text -> theory -> theory
    1.18 +  val add_subsubsection: Comment.text -> theory -> theory
    1.19    val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
    1.20    val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    1.21    val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
    1.22 @@ -105,7 +105,7 @@
    1.23  
    1.24  (* formal comments *)   (* FIXME dummy *)
    1.25  
    1.26 -fun add_text (txt:string) (thy:theory) = thy;
    1.27 +fun add_text _ thy = thy;
    1.28  fun add_title title author date thy = thy;
    1.29  val add_chapter = add_text;
    1.30  val add_section = add_text;