# HG changeset patch
# User berghofe
# Date 1188467197 -7200
# Node ID 5edb9a54900f0b837cdea867a9c1a7636066dc41
# Parent  c3a4a289decccf2d425321f0820fe9413dd27675
- tuned section about inductive predicates
- fixed broken railroad diagram in section about executable code

diff -r c3a4a289decc -r 5edb9a54900f doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Thu Aug 30 05:01:38 2007 +0200
+++ b/doc-src/IsarRef/logics.tex	Thu Aug 30 11:46:37 2007 +0200
@@ -603,7 +603,8 @@
 \end{matharray}
 
 \begin{rail}
-  ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\ ('where' clauses)? ('monos' thmrefs)?
+  ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
+  ('where' clauses)? ('monos' thmrefs)?
   ;
   clauses: (thmdecl? prop + '|')
   ;
@@ -614,6 +615,8 @@
 \begin{descr}
 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
   (co)inductive predicates from the introduction rules given in the \texttt{where} section.
+  The optional \texttt{for} section contains a list of parameters of the (co)inductive
+  predicates that remain fixed throughout the definition.
   The optional \texttt{monos} section contains \textit{monotonicity theorems},
   which are required for each operator applied to a recursive set in the introduction rules.
   There {\bf must} be a theorem of the form $A \leq B \Imp M~A \leq M~B$, for each
@@ -728,7 +731,7 @@
   ;
   inducttac goalspec? (insts * 'and') rule?
   ;
-  indcases (prop +)
+  indcases (prop +) ('for' (name +)) ?
   ;
   inductivecases (thmdecl? (prop +) + 'and')
   ;
@@ -752,7 +755,9 @@
 
   While $ind_cases$ is a proof method to apply the result immediately as
   elimination rules, $\isarkeyword{inductive_cases}$ provides case split
-  theorems at the theory level for later use,
+  theorems at the theory level for later use.
+  The \texttt{for} option of the $ind_cases$ method allows to specify a list
+  of variables that should be generalized before applying the resulting rule.
 \end{descr}
 
 
@@ -863,7 +868,8 @@
 
 \begin{rail}
 'export\_code' ( constexpr + ) ? \\
-  ( ( 'in' target ( 'module_name' string ) ? ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
+  ( ( 'in' target ( 'module\_name' string ) ? \\
+      ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
 
 'code\_thms' ( constexpr + ) ?;