--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 17 13:50:02 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 17 06:49:23 2010 -0800
@@ -89,7 +89,7 @@
lemma "Rep_unit () = True"
nitpick [expect = none]
-by (insert Rep_unit) (simp add: unit_def)
+by (insert Rep_unit) simp
lemma "Rep_unit () = False"
nitpick [expect = genuine]
--- a/src/HOL/Product_Type.thy Wed Nov 17 13:50:02 2010 +0100
+++ b/src/HOL/Product_Type.thy Wed Nov 17 06:49:23 2010 -0800
@@ -37,7 +37,7 @@
subsection {* The @{text unit} type *}
-typedef unit = "{True}"
+typedef (open) unit = "{True}"
proof
show "True : ?unit" ..
qed
@@ -48,7 +48,7 @@
"() = Abs_unit True"
lemma unit_eq [no_atp]: "u = ()"
- by (induct u) (simp add: unit_def Unity_def)
+ by (induct u) (simp add: Unity_def)
text {*
Simplification procedure for @{thm [source] unit_eq}. Cannot use
--- a/src/HOLCF/ConvexPD.thy Wed Nov 17 13:50:02 2010 +0100
+++ b/src/HOLCF/ConvexPD.thy Wed Nov 17 06:49:23 2010 -0800
@@ -360,6 +360,11 @@
lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit)
+lemma convex_bind_bind:
+ "convex_bind\<cdot>(convex_bind\<cdot>xs\<cdot>f)\<cdot>g =
+ convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_bind\<cdot>(f\<cdot>x)\<cdot>g)"
+by (induct xs, simp_all)
+
subsection {* Map *}
--- a/src/HOLCF/LowerPD.thy Wed Nov 17 13:50:02 2010 +0100
+++ b/src/HOLCF/LowerPD.thy Wed Nov 17 06:49:23 2010 -0800
@@ -353,6 +353,10 @@
lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit)
+lemma lower_bind_bind:
+ "lower_bind\<cdot>(lower_bind\<cdot>xs\<cdot>f)\<cdot>g = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_bind\<cdot>(f\<cdot>x)\<cdot>g)"
+by (induct xs, simp_all)
+
subsection {* Map *}
--- a/src/HOLCF/UpperPD.thy Wed Nov 17 13:50:02 2010 +0100
+++ b/src/HOLCF/UpperPD.thy Wed Nov 17 06:49:23 2010 -0800
@@ -348,6 +348,10 @@
lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit)
+lemma upper_bind_bind:
+ "upper_bind\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_bind\<cdot>(f\<cdot>x)\<cdot>g)"
+by (induct xs, simp_all)
+
subsection {* Map *}