# HG changeset patch
# User haftmann
# Date 1163428979 -3600
# Node ID a5089fc012b5db6a04e462c6504aae7bc0a07624
# Parent  74ab7c0980c7ef31a5575b9dee2c2b608bcb9f51
adjusted

diff -r 74ab7c0980c7 -r a5089fc012b5 doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Mon Nov 13 15:42:58 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Mon Nov 13 15:42:59 2006 +0100
@@ -330,7 +330,7 @@
   \indexml{betapply}\verb|betapply: term * term -> term| \\
   \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\
   \indexml{Sign.add-abbrevs}\verb|Sign.add_abbrevs: string * bool ->|\isasep\isanewline%
-\verb|  ((string * mixfix) * term) list -> theory -> theory| \\
+\verb|  ((string * mixfix) * term) list -> theory -> (term * term) list * theory| \\
   \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
   \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
   \end{mldecls}
diff -r 74ab7c0980c7 -r a5089fc012b5 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Mon Nov 13 15:42:58 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Mon Nov 13 15:42:59 2006 +0100
@@ -328,7 +328,7 @@
   @{index_ML betapply: "term * term -> term"} \\
   @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
   @{index_ML Sign.add_abbrevs: "string * bool ->
-  ((string * mixfix) * term) list -> theory -> theory"} \\
+  ((string * mixfix) * term) list -> theory -> (term * term) list * theory"} \\
   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   \end{mldecls}
diff -r 74ab7c0980c7 -r a5089fc012b5 doc-src/TutorialI/Overview/LNCS/FP1.thy
--- a/doc-src/TutorialI/Overview/LNCS/FP1.thy	Mon Nov 13 15:42:58 2006 +0100
+++ b/doc-src/TutorialI/Overview/LNCS/FP1.thy	Mon Nov 13 15:42:59 2006 +0100
@@ -1,4 +1,4 @@
-(*<*)theory FP1 = Main:(*>*)
+(*<*)theory FP1 imports Main begin(*>*)
 
 subsection{*Quickcheck*}
 
diff -r 74ab7c0980c7 -r a5089fc012b5 doc-src/TutorialI/Overview/LNCS/Ind.thy
--- a/doc-src/TutorialI/Overview/LNCS/Ind.thy	Mon Nov 13 15:42:58 2006 +0100
+++ b/doc-src/TutorialI/Overview/LNCS/Ind.thy	Mon Nov 13 15:42:59 2006 +0100
@@ -1,4 +1,4 @@
-(*<*)theory Ind = Main:(*>*)
+(*<*)theory Ind imports Main begin(*>*)
 
 section{*Inductive Definitions*}
 
diff -r 74ab7c0980c7 -r a5089fc012b5 doc-src/TutorialI/Overview/LNCS/Rules.thy
--- a/doc-src/TutorialI/Overview/LNCS/Rules.thy	Mon Nov 13 15:42:58 2006 +0100
+++ b/doc-src/TutorialI/Overview/LNCS/Rules.thy	Mon Nov 13 15:42:59 2006 +0100
@@ -1,4 +1,4 @@
-(*<*)theory Rules = Main:(*>*)
+(*<*)theory Rules imports Main begin(*>*)
 
 section{*The Rules of the Game*}
 
diff -r 74ab7c0980c7 -r a5089fc012b5 doc-src/TutorialI/Overview/LNCS/Sets.thy
--- a/doc-src/TutorialI/Overview/LNCS/Sets.thy	Mon Nov 13 15:42:58 2006 +0100
+++ b/doc-src/TutorialI/Overview/LNCS/Sets.thy	Mon Nov 13 15:42:59 2006 +0100
@@ -1,4 +1,4 @@
-(*<*)theory Sets = Main:(*>*)
+(*<*)theory Sets imports Main begin(*>*)
 
 section{*Sets, Functions and Relations*}