# HG changeset patch
# User blanchet
# Date 1379512575 -7200
# Node ID 7b453b619b5f2fe8d7f24a5b6ad5dae2af1cd642
# Parent  71b020d161c5ae5096932ae6b7a7d5fe641bf2af
use singular to avoid confusion

diff -r 71b020d161c5 -r 7b453b619b5f src/Doc/Datatypes/Datatypes.thy
--- 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}
diff -r 71b020d161c5 -r 7b453b619b5f src/HOL/BNF/Examples/Process.thy
--- 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) *}
diff -r 71b020d161c5 -r 7b453b619b5f src/HOL/BNF/Examples/Stream.thy
--- 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)"
diff -r 71b020d161c5 -r 7b453b619b5f src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- 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], []),
diff -r 71b020d161c5 -r 7b453b619b5f src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- 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),
diff -r 71b020d161c5 -r 7b453b619b5f src/HOL/BNF/Tools/bnf_fp_util.ML
--- 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"