# HG changeset patch
# User haftmann
# Date 1276521036 -7200
# Node ID c88c4415608381c891e5fce71136f6fa7ae8cb87
# Parent  fe6262d929a3090133e14b5d8b213d3d6b0504f7
removed simplifier congruence rule of "prod_case"

diff -r fe6262d929a3 -r c88c44156083 NEWS
--- a/NEWS	Fri Jun 11 16:52:17 2010 +0200
+++ b/NEWS	Mon Jun 14 15:10:36 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)
 ---------------------------------
diff -r fe6262d929a3 -r c88c44156083 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Jun 11 16:52:17 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Jun 14 15:10:36 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
diff -r fe6262d929a3 -r c88c44156083 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Jun 11 16:52:17 2010 +0200
+++ b/src/HOL/Product_Type.thy	Mon Jun 14 15:10:36 2010 +0200
@@ -158,6 +158,8 @@
     by (simp add: Pair_def Abs_prod_inject)
 qed
 
+declare weak_case_cong [cong del]
+
 
 subsubsection {* Tuple syntax *}