# 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 \ { 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 \ { 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 *}