--- 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]}