# HG changeset patch
# User blanchet
# Date 1392937795 -3600
# Node ID 5b466efedd2c76f01fdc1ae60cfa8eb4b2f041a6
# Parent  abc140f21caab683e6adb8e06fb3015cbbb21a41
renamed 'recs' and 'cases' theorems 'rec' and 'case' in old datatype package, for consistency with new package

diff -r abc140f21caa -r 5b466efedd2c src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Feb 20 23:46:40 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Feb 21 00:09:55 2014 +0100
@@ -992,13 +992,12 @@
 that unfold the definition of constants introduced by \keyw{datatype} will be
 difficult to port.
 
-\item \emph{A few theorems have different names.}
-The properties @{text t.cases} and @{text t.recs} have been renamed
-@{text t.case} and @{text t.rec}. For non-mutually recursive datatypes,
-@{text t.inducts} is available as @{text t.induct}.
+\item \emph{Some induction rules have different names.}
+For non-mutually recursive datatypes,
+the alias @{text t.inducts} for @{text t.induct} is no longer generated.
 For $m > 1$ mutually recursive datatypes,
 @{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
-@{text "t\<^sub>i.induct"}.
+@{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, t}"}.
 
 \item \emph{The @{text t.simps} collection has been extended.}
 Previously available theorems are available at the same index.
diff -r abc140f21caa -r 5b466efedd2c src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Feb 20 23:46:40 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Feb 21 00:09:55 2014 +0100
@@ -258,7 +258,7 @@
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
     |> Global_Theory.note_thmss ""
-      [((Binding.name "recs", [Nitpick_Simps.add]), [(rec_thms, [])])]
+      [((Binding.name "rec", [Nitpick_Simps.add]), [(rec_thms, [])])]
     ||> Sign.parent_path
     |-> (fn thms => pair (reccomb_names, maps #2 thms))
   end;
@@ -349,7 +349,7 @@
     thy2
     |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
     |> Sign.parent_path
-    |> Datatype_Aux.store_thmss "cases" new_type_names case_thms
+    |> Datatype_Aux.store_thmss "case" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))
   end;