# HG changeset patch
# User wenzelm
# Date 911998843 -3600
# Node ID 7af99477751b3e56cd0f23e28b07c35e6e2dded5
# Parent  c48efb523a4df71f6e9c5d896959c9cce030c2f7
add_text, add_chapter etc.: dummy;

diff -r c48efb523a4d -r 7af99477751b src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Nov 25 14:00:12 1998 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Wed Nov 25 14:00:43 1998 +0100
@@ -12,6 +12,11 @@
 
 signature ISAR_THY =
 sig
+  val add_text: 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
   val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
   val have_theorems: (bstring * Args.src list) * (xstring * Args.src list) list
@@ -63,6 +68,15 @@
 
 (** derived theory and proof operations **)
 
+(* formal comments *)	(* FIXME dummy *)
+
+fun add_text (txt:string) (thy:theory) = thy;
+val add_chapter = add_text;
+val add_section = add_text;
+val add_subsection = add_text;
+val add_subsubsection = add_text;
+
+
 (* axioms and defs *)
 
 fun add_axms f args thy =