--- a/src/Doc/Datatypes/Datatypes.thy Tue Nov 19 14:11:26 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Nov 19 14:33:20 2013 +0100
@@ -350,7 +350,7 @@
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},
-@{text list_set}, @{text list_map}, and @{text list_rel}:
+@{text set_list}, @{text map_list}, and @{text rel_list}:
*}
(*<*)
@@ -501,7 +501,7 @@
reference manual \cite{isabelle-isar-ref}.
The optional names preceding the type variables allow to override the default
-names of the set functions (@{text t_set1}, \ldots, @{text t_setM}).
+names of the set functions (@{text set1_t}, \ldots, @{text setM_t}).
Inside a mutually recursive specification, all defined datatypes must
mention exactly the same type variables in the same order.
@@ -626,7 +626,7 @@
\begin{itemize}
\setlength{\itemsep}{0pt}
-\item \relax{Case combinator}: @{text t_case} (rendered using the familiar
+\item \relax{Case combinator}: @{text t.t_case} (rendered using the familiar
@{text case}--@{text of} syntax)
\item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
@@ -638,22 +638,22 @@
\phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
\item \relax{Set functions} (or \relax{natural transformations}):
-@{text t_set1}, \ldots, @{text t_setm}
-
-\item \relax{Map function} (or \relax{functorial action}): @{text t_map}
-
-\item \relax{Relator}: @{text t_rel}
-
-\item \relax{Iterator}: @{text t_fold}
-
-\item \relax{Recursor}: @{text t_rec}
+@{text set1_t}, \ldots, @{text t.setm_t}
+
+\item \relax{Map function} (or \relax{functorial action}): @{text t.map_t}
+
+\item \relax{Relator}: @{text t.rel_t}
+
+\item \relax{Iterator}: @{text t.t_fold}
+
+\item \relax{Recursor}: @{text t.t_rec}
\end{itemize}
\noindent
The case combinator, discriminators, and selectors are collectively called
\emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
-name and is normally hidden.
+names and is normally hidden.
*}
@@ -810,8 +810,8 @@
\item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\
@{thm list.sel_split_asm[no_vars]}
-\item[@{text "t."}\hthm{case\_if}\rm:] ~ \\
-@{thm list.case_if[no_vars]}
+\item[@{text "t."}\hthm{case\_eq\_if}\rm:] ~ \\
+@{thm list.case_eq_if[no_vars]}
\end{description}
\end{indentblock}
@@ -1150,13 +1150,13 @@
\noindent
The next example features recursion through the @{text option} type. Although
@{text option} is not a new-style datatype, it is registered as a BNF with the
-map function @{const option_map}:
+map function @{const map_option}:
*}
primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
"sum_btree (BNode a lt rt) =
- a + the_default 0 (option_map sum_btree lt) +
- the_default 0 (option_map sum_btree rt)"
+ a + the_default 0 (map_option sum_btree lt) +
+ the_default 0 (map_option sum_btree rt)"
text {*
\noindent
--- a/src/HOL/Tools/ctr_sugar.ML Tue Nov 19 14:11:26 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML Tue Nov 19 14:33:20 2013 +0100
@@ -30,7 +30,7 @@
expands: thm list,
sel_splits: thm list,
sel_split_asms: thm list,
- case_ifs: thm list};
+ case_eq_ifs: thm list};
val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar
@@ -90,7 +90,7 @@
expands: thm list,
sel_splits: thm list,
sel_split_asms: thm list,
- case_ifs: thm list};
+ case_eq_ifs: thm list};
fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
{ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
@@ -98,7 +98,7 @@
fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
- disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_ifs} =
+ disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_eq_ifs} =
{ctrs = map (Morphism.term phi) ctrs,
casex = Morphism.term phi casex,
discs = map (Morphism.term phi) discs,
@@ -121,7 +121,7 @@
expands = map (Morphism.thm phi) expands,
sel_splits = map (Morphism.thm phi) sel_splits,
sel_split_asms = map (Morphism.thm phi) sel_split_asms,
- case_ifs = map (Morphism.thm phi) case_ifs};
+ case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
val transfer_ctr_sugar =
morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
@@ -160,7 +160,7 @@
val caseN = "case";
val case_congN = "case_cong";
-val case_ifN = "case_if";
+val case_eq_ifN = "case_eq_if";
val collapseN = "collapse";
val disc_excludeN = "disc_exclude";
val disc_exhaustN = "disc_exhaust";
@@ -657,7 +657,7 @@
val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms,
- safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_if_thms) =
+ safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
if no_discs_sels then
([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
else
@@ -861,12 +861,12 @@
(thm, asm_thm)
end;
- val case_if_thm =
+ val case_eq_if_thm =
let
val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_case_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
+ mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy)
end;
@@ -874,7 +874,7 @@
(all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
- [sel_split_asm_thm], [case_if_thm])
+ [sel_split_asm_thm], [case_eq_if_thm])
end;
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
@@ -890,7 +890,7 @@
val notes =
[(caseN, case_thms, code_nitpicksimp_simp_attrs),
(case_congN, [case_cong_thm], []),
- (case_ifN, case_if_thms, []),
+ (case_eq_ifN, case_eq_if_thms, []),
(collapseN, safe_collapse_thms, simp_attrs),
(discN, nontriv_disc_thms, simp_attrs),
(discIN, nontriv_discI_thms, []),
@@ -921,7 +921,7 @@
discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
- case_ifs = case_if_thms};
+ case_eq_ifs = case_eq_if_thms};
in
(ctr_sugar,
lthy