# HG changeset patch
# User berghofe
# Date 1210150600 -7200
# Node ID a9134a089106863342cd2e782df27493c3dcd0da
# Parent  a6cb51c314f2ab56125e2b58eeddc3a250927b27
split_beta is now declared as monotonicity rule, to allow bounded
quantifiers in introduction rules of inductive predicates.

diff -r a6cb51c314f2 -r a9134a089106 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed May 07 10:56:39 2008 +0200
+++ b/src/HOL/Product_Type.thy	Wed May 07 10:56:40 2008 +0200
@@ -476,7 +476,7 @@
 Addsimprocs [split_beta_proc, split_eta_proc];
 *}
 
-lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)"
+lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
   by (subst surjective_pairing, rule split_conv)
 
 lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"