--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Readme.thy	Wed Oct 29 21:46:33 2008 +0100
@@ -0,0 +1,45 @@
+theory Readme
+imports Base
+begin
+
+chapter {* Comments for Authors of the Cookbook *}
+
+text {*
+
+  \begin{itemize}
+  \item You can make references to other Isabelle manuals using the 
+  reference names from those manuals. For this the following
+  four latex commands are defined:
+  
+  \begin{center}
+  \begin{tabular}{l|c|c}
+   & Chapters & Sections\\\hline
+  Implementation Manual & @{ML_text "\\ichcite{\<dots>}"} & @{ML_text "\\isccite{\<dots>}"}\\
+  Isar Reference Manual & @{ML_text "\\rchcite{\<dots>}"} & @{ML_text "\\rsccite{\<dots>}"}\\
+  \end{tabular}
+  \end{center}
+
+  So @{ML_text "\\ichcite{ch:logic}"} results in a reference for the chapter about logic 
+  in the implementation manual, namely \ichcite{ch:logic}.
+
+  \item There are various document antiquotations defined for the 
+  cookbook so that written text can be kept in sync with the 
+  Isabelle code and also that responses of the ML-compiler can be shown.
+  For example
+
+  \begin{itemize}
+  \item[$\bullet$] @{text "@{ML \"\<dots>\"}"}
+  \item[$\bullet$] @{text "@{ML_open \"\<dots>\"}"}
+  \item[$\bullet$] @{text "@{ML_response \"\<dots>\"}"}
+  \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\"}"}
+  \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"}
+  \end{itemize}
+
+  (FIXME: explain their usage)
+
+  \end{itemize}
+
+*}
+
+
+end
\ No newline at end of file