--- a/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 17:19:58 2014 +0200
@@ -773,8 +773,8 @@
\item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\
@{thm list.case_cong[no_vars]}
-\item[@{text "t."}\hthm{weak_case_cong} @{text "[cong]"}\rm:] ~ \\
-@{thm list.weak_case_cong[no_vars]}
+\item[@{text "t."}\hthm{case_cong_weak} @{text "[cong]"}\rm:] ~ \\
+@{thm list.case_cong_weak[no_vars]}
\item[@{text "t."}\hthm{split}\rm:] ~ \\
@{thm list.split[no_vars]}
@@ -809,27 +809,27 @@
@{thm list.collapse(1)[no_vars]} \\
@{thm list.collapse(2)[no_vars]}
-\item[@{text "t."}\hthm{disc_exclude} @{text "[dest]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\
These properties are missing for @{typ "'a list"} because there is only one
proper discriminator. Had the datatype been introduced with a second
discriminator called @{const nonnull}, they would have read thusly: \\[\jot]
@{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
@{prop "nonnull list \<Longrightarrow> \<not> null list"}
-\item[@{text "t."}\hthm{disc_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
-@{thm list.disc_exhaust[no_vars]}
-
-\item[@{text "t."}\hthm{sel_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
-@{thm list.sel_exhaust[no_vars]}
+\item[@{text "t."}\hthm{exhaust_disc} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
+@{thm list.exhaust_disc[no_vars]}
+
+\item[@{text "t."}\hthm{exhaust_sel} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
+@{thm list.exhaust_sel[no_vars]}
\item[@{text "t."}\hthm{expand}\rm:] ~ \\
@{thm list.expand[no_vars]}
-\item[@{text "t."}\hthm{sel_split}\rm:] ~ \\
-@{thm list.sel_split[no_vars]}
-
-\item[@{text "t."}\hthm{sel_split_asm}\rm:] ~ \\
-@{thm list.sel_split_asm[no_vars]}
+\item[@{text "t."}\hthm{split_sel}\rm:] ~ \\
+@{thm list.split_sel[no_vars]}
+
+\item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
+@{thm list.split_sel_asm[no_vars]}
\item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
@{thm list.case_eq_if[no_vars]}
@@ -868,18 +868,18 @@
@{thm list.set_intros(1)[no_vars]} \\
@{thm list.set_intros(2)[no_vars]}
-\item[@{text "t."}\hthm{sel_set}\rm:] ~ \\
-@{thm list.sel_set[no_vars]}
+\item[@{text "t."}\hthm{set_sel}\rm:] ~ \\
+@{thm list.set_sel[no_vars]}
\item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.map(1)[no_vars]} \\
@{thm list.map(2)[no_vars]}
-\item[@{text "t."}\hthm{disc_map_iff} @{text "[simp]"}\rm:] ~ \\
-@{thm list.disc_map_iff[no_vars]}
-
-\item[@{text "t."}\hthm{sel_map}\rm:] ~ \\
-@{thm list.sel_map[no_vars]}
+\item[@{text "t."}\hthm{map_disc_iff} @{text "[simp]"}\rm:] ~ \\
+@{thm list.map_disc_iff[no_vars]}
+
+\item[@{text "t."}\hthm{map_sel}\rm:] ~ \\
+@{thm list.map_sel[no_vars]}
\item[@{text "t."}\hthm{rel_inject} @{text "[simp]"}\rm:] ~ \\
@{thm list.rel_inject(1)[no_vars]} \\
@@ -1772,10 +1772,10 @@
@{thm llist.coinduct[no_vars]}
\item[\begin{tabular}{@ {}l@ {}}
- @{text "t."}\hthm{strong_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
- \phantom{@{text "t."}\hthm{strong_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
+ @{text "t."}\hthm{coinduct_strong} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
+ \phantom{@{text "t."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
\end{tabular}] ~ \\
-@{thm llist.strong_coinduct[no_vars]}
+@{thm llist.coinduct_strong[no_vars]}
\item[\begin{tabular}{@ {}l@ {}}
@{text "t."}\hthm{rel_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
@@ -1786,8 +1786,8 @@
\item[\begin{tabular}{@ {}l@ {}}
@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m, case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"} \\
- @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
- \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
+ @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
+ \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
\phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
\end{tabular}] ~ \\
@@ -1808,17 +1808,17 @@
\item[@{text "t."}\hthm{corec_code} @{text "[code]"}\rm:] ~ \\
@{thm llist.corec_code[no_vars]}
-\item[@{text "t."}\hthm{disc_corec}\rm:] ~ \\
-@{thm llist.disc_corec(1)[no_vars]} \\
-@{thm llist.disc_corec(2)[no_vars]}
-
-\item[@{text "t."}\hthm{disc_corec_iff} @{text "[simp]"}\rm:] ~ \\
-@{thm llist.disc_corec_iff(1)[no_vars]} \\
-@{thm llist.disc_corec_iff(2)[no_vars]}
-
-\item[@{text "t."}\hthm{sel_corec} @{text "[simp]"}\rm:] ~ \\
-@{thm llist.sel_corec(1)[no_vars]} \\
-@{thm llist.sel_corec(2)[no_vars]}
+\item[@{text "t."}\hthm{corec_disc}\rm:] ~ \\
+@{thm llist.corec_disc(1)[no_vars]} \\
+@{thm llist.corec_disc(2)[no_vars]}
+
+\item[@{text "t."}\hthm{corec_disc_iff} @{text "[simp]"}\rm:] ~ \\
+@{thm llist.corec_disc_iff(1)[no_vars]} \\
+@{thm llist.corec_disc_iff(2)[no_vars]}
+
+\item[@{text "t."}\hthm{corec_sel} @{text "[simp]"}\rm:] ~ \\
+@{thm llist.corec_sel(1)[no_vars]} \\
+@{thm llist.corec_sel(2)[no_vars]}
\end{description}
\end{indentblock}
@@ -1829,7 +1829,7 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec_iff}] @{text t.sel_corec} ~ \\
+\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec_disc_iff}] @{text t.corec_sel} ~ \\
@{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
\end{description}
@@ -2151,7 +2151,7 @@
@{thm [source] iterate\<^sub>i\<^sub>i.coinduct},
@{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 strong_coinduct}. These rules and the
+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
to speed up subsequent definitions.
*}