--- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 18 15:33:32 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Sep 18 15:56:15 2013 +0200
@@ -750,13 +750,13 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{discs} @{text "[simp]"}\rm:] ~ \\
-@{thm list.discs(1)[no_vars]} \\
-@{thm list.discs(2)[no_vars]}
-
-\item[@{text "t."}\hthm{sels} @{text "[simp]"}\rm:] ~ \\
-@{thm list.sels(1)[no_vars]} \\
-@{thm list.sels(2)[no_vars]}
+\item[@{text "t."}\hthm{disc} @{text "[simp]"}\rm:] ~ \\
+@{thm list.disc(1)[no_vars]} \\
+@{thm list.disc(2)[no_vars]}
+
+\item[@{text "t."}\hthm{sel} @{text "[simp]"}\rm:] ~ \\
+@{thm list.sel(1)[no_vars]} \\
+@{thm list.sel(2)[no_vars]}
\item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
@{thm list.collapse(1)[no_vars]} \\
@@ -792,9 +792,9 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{sets} @{text "[code]"}\rm:] ~ \\
-@{thm list.sets(1)[no_vars]} \\
-@{thm list.sets(2)[no_vars]}
+\item[@{text "t."}\hthm{set} @{text "[code]"}\rm:] ~ \\
+@{thm list.set(1)[no_vars]} \\
+@{thm list.set(2)[no_vars]}
\item[@{text "t."}\hthm{map} @{text "[code]"}\rm:] ~ \\
@{thm list.map(1)[no_vars]} \\
@@ -847,7 +847,7 @@
\begin{description}
\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\
-@{text t.rel_distinct} @{text t.sets}
+@{text t.rel_distinct} @{text t.set}
\end{description}
\end{indentblock}
@@ -1547,7 +1547,7 @@
\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec}$^*$ @{text t.disc_corec}] ~ \\
@{text t.disc_corec_iff} @{text t.sel_corec} @{text t.unfold}$^*$ @{text t.disc_unfold} @{text t.disc_unfold_iff} ~ \\
-@{text t.sel_unfold} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.sets}
+@{text t.sel_unfold} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
\end{description}
\end{indentblock}
--- a/src/HOL/BNF/Examples/Process.thy Wed Sep 18 15:33:32 2013 +0200
+++ b/src/HOL/BNF/Examples/Process.thy Wed Sep 18 15:56:15 2013 +0200
@@ -44,7 +44,7 @@
Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> \<phi> p p' \<and> \<phi> q q'"
shows "p = p'"
using assms
- by (coinduct rule: process.coinduct) (metis process.collapse(1,2) process.discs(3))
+ by (coinduct rule: process.coinduct) (metis process.collapse(1,2) process.disc(3))
(* Stronger coinduction, up to equality: *)
theorem process_strong_coind[elim, consumes 1, case_names iss Action Choice]:
@@ -54,7 +54,7 @@
Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> q = q')"
shows "p = p'"
using assms
- by (coinduct rule: process.strong_coinduct) (metis process.collapse(1,2) process.discs(3))
+ by (coinduct rule: process.strong_coinduct) (metis process.collapse(1,2) process.disc(3))
subsection {* Coiteration (unfold) *}
--- a/src/HOL/BNF/Examples/Stream.thy Wed Sep 18 15:33:32 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy Wed Sep 18 15:56:15 2013 +0200
@@ -33,7 +33,7 @@
*}
code_datatype Stream
-lemmas [code] = stream.sels stream.sets stream.case
+lemmas [code] = stream.sel stream.set stream.case
lemma stream_case_cert:
assumes "CASE \<equiv> stream_case c"
@@ -495,7 +495,7 @@
lemma sinterleave_code[code]:
"sinterleave (x ## s1) s2 = x ## sinterleave s2 s1"
- by (metis sinterleave_simps stream.exhaust stream.sels)
+ by (metis sinterleave_simps stream.exhaust stream.sel)
lemma sinterleave_snth[simp]:
"even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 18 15:33:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 18 15:56:15 2013 +0200
@@ -115,13 +115,13 @@
val collapseN = "collapse";
val disc_excludeN = "disc_exclude";
val disc_exhaustN = "disc_exhaust";
-val discsN = "discs";
+val discN = "disc";
val distinctN = "distinct";
val exhaustN = "exhaust";
val expandN = "expand";
val injectN = "inject";
val nchotomyN = "nchotomy";
-val selsN = "sels";
+val selN = "sel";
val splitN = "split";
val splitsN = "splits";
val split_asmN = "split_asm";
@@ -750,7 +750,7 @@
(case_congN, [case_cong_thm], []),
(case_convN, case_conv_thms, []),
(collapseN, collapse_thms, simp_attrs),
- (discsN, disc_thms, simp_attrs),
+ (discN, disc_thms, simp_attrs),
(disc_excludeN, disc_exclude_thms, []),
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
(distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
@@ -758,7 +758,7 @@
(expandN, expand_thms, []),
(injectN, inject_thms, iff_attrs @ induct_simp_attrs),
(nchotomyN, [nchotomy_thm], []),
- (selsN, all_sel_thms, simp_attrs),
+ (selN, all_sel_thms, simp_attrs),
(splitN, [split_thm], []),
(split_asmN, [split_asm_thm], []),
(splitsN, [split_thm, split_asm_thm], []),
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Sep 18 15:33:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Sep 18 15:56:15 2013 +0200
@@ -1395,7 +1395,7 @@
[(mapN, map_thms, code_simp_attrs),
(rel_distinctN, rel_distinct_thms, code_simp_attrs),
(rel_injectN, rel_inject_thms, code_simp_attrs),
- (setsN, flat set_thmss, code_simp_attrs)]
+ (setN, flat set_thmss, code_simp_attrs)]
|> massage_simple_notes fp_b_name;
in
(((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar),
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Sep 18 15:33:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Sep 18 15:56:15 2013 +0200
@@ -111,7 +111,7 @@
val set_inclN: string
val set_set_inclN: string
val sel_unfoldN: string
- val setsN: string
+ val setN: string
val simpsN: string
val strTN: string
val str_initN: string
@@ -287,7 +287,7 @@
val LevN = "Lev"
val rvN = "recover"
val behN = "beh"
-val setsN = "sets"
+val setN = "set"
val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN
val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN
fun mk_set_inductN i = mk_setN i ^ "_induct"