# HG changeset patch
# User blanchet
# Date 1392222959 -3600
# Node ID 17fb554688f0dce45fdbd9f6e69fba3328ae3533
# Parent  b445c39cc7e98ffbf7f83fc587b0de38129a5c2c
tuning

diff -r b445c39cc7e9 -r 17fb554688f0 src/HOL/List.thy
--- 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
diff -r b445c39cc7e9 -r 17fb554688f0 src/HOL/Option.thy
--- 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
diff -r b445c39cc7e9 -r 17fb554688f0 src/HOL/Product_Type.thy
--- 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
diff -r b445c39cc7e9 -r 17fb554688f0 src/HOL/Sum_Type.thy
--- 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