author haftmann Mon, 14 Jun 2010 15:10:36 +0200 changeset 37411 c88c44156083 parent 37395 fe6262d929a3 child 37412 8cd75d103af9
removed simplifier congruence rule of "prod_case"
 NEWS file | annotate | diff | comparison | revisions src/HOL/Decision_Procs/Approximation.thy file | annotate | diff | comparison | revisions src/HOL/Product_Type.thy file | annotate | diff | comparison | revisions
```--- 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)
---------------------------------```
```--- 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```
```--- 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 @@