--- a/NEWS Mon Jun 14 10:36:01 2010 +0200
+++ b/NEWS Mon Jun 14 15:10:50 2010 +0200
@@ -25,6 +25,9 @@
INCOMPATIBILITY.
+* Removed simplifier congruence rule of "prod_case", as has for long
+been the case with "split".
+
New in Isabelle2009-2 (June 2010)
---------------------------------
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Jun 14 10:36:01 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Jun 14 15:10:50 2010 +0200
@@ -2552,9 +2552,7 @@
where l_eq: "Some (l, u') = approx prec a vs"
and u_eq: "Some (l', u) = approx prec b vs"
and approx_form': "approx_form' prec f (ss ! n) n l u vs ss"
- by (cases "approx prec a vs", simp,
- cases "approx prec b vs", auto) blast
-
+ by (cases "approx prec a vs", simp) (cases "approx prec b vs", auto)
{ assume "xs ! n \<in> { interpret_floatarith a xs .. interpret_floatarith b xs }"
with approx[OF Bound.prems(2) l_eq] and approx[OF Bound.prems(2) u_eq]
have "xs ! n \<in> { real l .. real u}" by auto
--- a/src/HOL/Product_Type.thy Mon Jun 14 10:36:01 2010 +0200
+++ b/src/HOL/Product_Type.thy Mon Jun 14 15:10:50 2010 +0200
@@ -158,6 +158,8 @@
by (simp add: Pair_def Abs_prod_inject)
qed
+declare weak_case_cong [cong del]
+
subsubsection {* Tuple syntax *}