--- a/src/HOL/List.thy Wed Feb 12 16:35:58 2014 +0100
+++ b/src/HOL/List.thy Wed Feb 12 17:35:59 2014 +0100
@@ -14,8 +14,6 @@
datatype_new_compat list
-thm list.exhaust[no_vars]
-
lemma [case_names Nil Cons, cases type: list]:
-- {* for backward compatibility -- names of variables differ *}
"(y = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>a list. y = a # list \<Longrightarrow> P) \<Longrightarrow> P"
@@ -26,7 +24,8 @@
"P [] \<Longrightarrow> (\<And>a list. P list \<Longrightarrow> P (a # list)) \<Longrightarrow> P list"
by (rule list.induct)
--- {* Compatibility *}
+text {* Compatibility: *}
+
setup {* Sign.mandatory_path "list" *}
lemmas inducts = list.induct
--- a/src/HOL/Option.thy Wed Feb 12 16:35:58 2014 +0100
+++ b/src/HOL/Option.thy Wed Feb 12 17:35:59 2014 +0100
@@ -24,7 +24,8 @@
"P None \<Longrightarrow> (\<And>option. P (Some option)) \<Longrightarrow> P option"
by (rule option.induct)
--- {* Compatibility *}
+text {* Compatibility: *}
+
setup {* Sign.mandatory_path "option" *}
lemmas inducts = option.induct
--- a/src/HOL/Product_Type.thy Wed Feb 12 16:35:58 2014 +0100
+++ b/src/HOL/Product_Type.thy Wed Feb 12 17:35:59 2014 +0100
@@ -15,14 +15,16 @@
wrap_free_constructors [True, False] case_bool [=]
by auto
--- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+
setup {* Sign.mandatory_path "old" *}
rep_datatype True False by (auto intro: bool_induct)
setup {* Sign.parent_path *}
--- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+
setup {* Sign.mandatory_path "bool" *}
lemmas induct = old.bool.induct
@@ -83,14 +85,16 @@
wrap_free_constructors ["()"] case_unit
by auto
--- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+
setup {* Sign.mandatory_path "old" *}
rep_datatype "()" by simp
setup {* Sign.parent_path *}
--- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+
setup {* Sign.mandatory_path "unit" *}
lemmas induct = old.unit.induct
@@ -195,7 +199,8 @@
by (simp add: Pair_def Abs_prod_inject)
qed
--- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+
setup {* Sign.mandatory_path "old" *}
rep_datatype Pair
@@ -203,7 +208,8 @@
setup {* Sign.parent_path *}
--- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+
setup {* Sign.mandatory_path "prod" *}
declare
--- a/src/HOL/Sum_Type.thy Wed Feb 12 16:35:58 2014 +0100
+++ b/src/HOL/Sum_Type.thy Wed Feb 12 17:35:59 2014 +0100
@@ -88,7 +88,8 @@
wrap_free_constructors [Inl, Inr] case_sum [isl] [[projl], [projr]]
by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
--- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+
setup {* Sign.mandatory_path "old" *}
rep_datatype Inl Inr
@@ -101,7 +102,8 @@
setup {* Sign.parent_path *}
--- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+
setup {* Sign.mandatory_path "sum" *}
declare