--- a/CookBook/Package/Ind_Interface.thy	Tue Feb 17 13:53:54 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Wed Feb 18 17:17:37 2009 +0000
@@ -8,6 +8,25 @@
   The purpose of the package we show next is that the user just specifies the
   inductive predicate by stating some introduction rules and then the packages
   makes the equivalent definition and derives from it the needed properties.
+*}
+
+text {*
+  From a high-level perspective the package consists of 6 subtasks:
+
+  \begin{itemize}
+  \item reading the various parts of specification (i.e.~parser),
+  \item transforming the parser outut into an internal 
+  (typed) datastructure,
+  \item making the definitions, 
+  \item deriving the induction principles,
+  \item deriving the introduction rules, and
+  \item storing the results in the given theory. 
+  to the user. 
+  \end{itemize}
+
+*}
+
+text {* 
   To be able to write down the specification in Isabelle, we have to introduce
   a new command (see Section~\ref{sec:newcommand}).  As the keyword for the new
   command we chose \simpleinductive{}. The specifications corresponding to our
@@ -83,22 +102,6 @@
 *}
 
 text {*
-  From a high-level perspective the package consists of 6 subtasks:
-
-  \begin{itemize}
-  \item reading the various parts of specification (i.e.~parser),
-  \item transforming the parser outut into an internal 
-  (typed) datastructure,
-  \item making the definitions, 
-  \item deriving the induction principles,
-  \item deriving the introduction rules, and
-  \item storing the results in the given theory to be visible 
-  to the user. 
-  \end{itemize}
-
-*}
-
-text {*
   \begin{figure}[p]
   \begin{isabelle}
   \railnontermfont{\rmfamily\itshape}
@@ -232,7 +235,7 @@
 *}
 
 text {*
-  (FIXME: explain Binding.binding; mixfix; Attrib.src; Attrib.src somewhere else)
+  (FIXME: explain Binding.binding; Attrib.binding somewhere else)
 
 
   The function for external invocation of the package is called @{ML