--- a/ProgTutorial/Package/Ind_Interface.thy	Thu Jul 30 11:38:52 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Thu Jul 30 15:51:51 2009 +0200
@@ -50,40 +50,14 @@
 \end{figure}  
 *}
 
-text {*
-  \begin{figure}[p]
-  \begin{boxedminipage}{\textwidth}
-  \begin{isabelle}
-  \railnontermfont{\rmfamily\itshape}
-  \railterm{simpleinductive,where,for}
-  \railalias{simpleinductive}{\simpleinductive{}}
-  \railalias{where}{\isacommand{where}}
-  \railalias{for}{\isacommand{for}}
-  \begin{rail}
-  simpleinductive target?\\ fixes
-  (where (thmdecl? prop + '|'))?
-  ;
-  \end{rail}
-  \end{isabelle}
-  \end{boxedminipage}
-  \caption{A railroad diagram describing the syntax of \simpleinductive{}. 
-  The \emph{target} indicates an optional locale; the \emph{fixes} are an 
-  \isacommand{and}-separated list of names for the inductive predicates (they
-  can also contain typing- and syntax annotations); \emph{prop} stands for a 
-  introduction rule with an optional theorem declaration (\emph{thmdecl}).
-  \label{fig:railroad}}
-  \end{figure}
-*}
+text {* 
+  To be able to write down the specifications of inductive predicates, we have
+  to introduce a new command (see Section~\ref{sec:newcommand}).  As the
+  keyword for the new command we chose \simpleinductive{}. Examples of
+  specifications from the previous section are shown in
+  Figure~\ref{fig:specs}. The syntax used in these examples more or
+  less translates directly into the parser:
 
-text {* 
-  To be able to write down the specifications or inductive predicates, we have 
-  to introduce
-  a new command (see Section~\ref{sec:newcommand}).  As the keyword for the
-  new command we chose \simpleinductive{}. Examples of specifications we expect
-  the user gives for the inductive predicates from the previous section are
-  shown in Figure~\ref{fig:specs}. The general syntax we will parse is specified
-  in the railroad diagram shown in Figure~\ref{fig:railroad}. This diagram more 
-  or less translates directly into the parser:
 *}
 
 ML{*val spec_parser = 
@@ -95,11 +69,11 @@
              (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 
 text {*
-  which we explained in Section~\ref{sec:parsingspecs}.  However, if you look
-  closely, there is no code for parsing the target given optionally after the
-  keyword. This is an ``advanced'' feature which we will inherit for ``free''
-  from the infrastructure on which we shall build the package. The target
-  stands for a locale and allows us to specify
+  which we explained in Section~\ref{sec:parsingspecs}.  There is no code included 
+  for parsing the keyword and what is called a \emph{target}. The latter  can be given 
+  optionally after the keyword. The target is an ``advanced'' feature which we will 
+  inherit for ``free'' from the infrastructure on which we shall build the package. 
+  The target stands for a locale and allows us to specify
 *}
 
 locale rel =
@@ -139,7 +113,7 @@
       \"where \" ^
       \"  even0[intro]: \\\"even 0\\\" \" ^ 
       \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
-      \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
+      \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\" \")
 in
   parse spec_parser input
 end"
@@ -151,8 +125,7 @@
   then we get back the specifications of the predicates (with type and syntax annotations), 
   and specifications of the introduction rules. This is all the information we
   need for calling the package and setting up the keyword. The latter is
-  done in Lines 5 to 7 in the code below.\footnote{FIXME: Is there a way to state 
-  here @{text "simple_inductive"}?}
+  done in Lines 5 to 7 in the code below.
 *}
 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy 
    fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*)