src/Doc/Datatypes/Datatypes.thy

--- a/src/Doc/Datatypes/Datatypes.thy	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Feb 23 16:50:10 2016 +0100
@@ -342,7 +342,7 @@
 text \<open>
 The @{command datatype} command introduces various constants in addition to
 the constructors. With each datatype are associated set functions, a map
-function,, a predicator, a relator, discriminators, and selectors, all of which can be given
+function, a predicator, a relator, discriminators, and selectors, all of which can be given
 custom names. In the example below, the familiar names @{text null}, @{text hd},
 @{text tl}, @{text set}, @{text map}, and @{text list_all2} override the
 default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2},
@@ -916,6 +916,10 @@
 \item[@{text "t."}\hthm{map_sel}\rm:] ~ \\
 @{thm list.map_sel[no_vars]}
 
+\item[@{text "t."}\hthm{pred_inject} @{text "[simp]"}\rm:] ~ \\
+@{thm list.pred_inject(1)[no_vars]} \\
+@{thm list.pred_inject(2)[no_vars]}
+
 \item[@{text "t."}\hthm{rel_inject} @{text "[simp]"}\rm:] ~ \\
 @{thm list.rel_inject(1)[no_vars]} \\
 @{thm list.rel_inject(2)[no_vars]}
@@ -1475,7 +1479,8 @@
 \<close>
 
     primrec increasing_tree :: "int \<Rightarrow> int tree\<^sub>f\<^sub>f \<Rightarrow> bool" where
-      "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \<longleftrightarrow> n \<ge> m \<and> list_all (increasing_tree (n + 1)) ts"
+      "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \<longleftrightarrow>
+       n \<ge> m \<and> list_all (increasing_tree (n + 1)) ts"
 
 
 subsubsection \<open> Nested-as-Mutual Recursion
@@ -1512,7 +1517,7 @@
 @{thm [source] at\<^sub>f\<^sub>f.induct},
 @{thm [source] ats\<^sub>f\<^sub>f.induct}, and
 @{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}. The
-induction rules and the underlying recursors are generated on a per-need basis
+induction rules and the underlying recursors are generated dynamically
 and are kept in a cache to speed up subsequent definitions.
 
 Here is a second example:
@@ -2352,7 +2357,7 @@
 @{thm [source] iterates\<^sub>i\<^sub>i.coinduct}, and
 @{thm [source] iterate\<^sub>i\<^sub>i_iterates\<^sub>i\<^sub>i.coinduct}
 and analogously for @{text coinduct_strong}. These rules and the
-underlying corecursors are generated on a per-need basis and are kept in a cache
+underlying corecursors are generated dynamically and are kept in a cache
 to speed up subsequent definitions.
 \<close>
 
@@ -2986,7 +2991,7 @@
   @@{command bnf} target? (name ':')? type \<newline>
     'map:' term ('sets:' (term +))? 'bd:' term \<newline>
     ('wits:' (term +))? ('rel:' term)? \<newline>
-    @{syntax plugins}?
+    ('pred:' term)? @{syntax plugins}?
 \<close>}
 
 \medskip
@@ -3404,11 +3409,6 @@
 \item[@{text "t."}\hthm{Domainp_rel} @{text "[relator_domain]"}\rm:] ~ \\
 @{thm list.Domainp_rel[no_vars]}
 
-\item[@{text "t."}\hthm{pred_inject} @{text "[simp]"}\rm:] ~ \\
-@{thm list.pred_inject(1)[no_vars]} \\
-@{thm list.pred_inject(2)[no_vars]} \\
-This property is generated only for (co)datatypes.
-
 \item[@{text "t."}\hthm{left_total_rel} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.left_total_rel[no_vars]}