# HG changeset patch
# User oheimb
# Date 896792820 -7200
# Node ID 8f4dc836a2ead02e0f24eb1c192072066276c0b5
# Parent  257aeccdefc3207dbb4a501bb0503443dea627b6
added split_sum_case_asm

diff -r 257aeccdefc3 -r 8f4dc836a2ea src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Fri May 29 13:50:21 1998 +0200
+++ b/src/HOL/Sum.ML	Tue Jun 02 15:07:00 1998 +0200
@@ -152,6 +152,11 @@
 by Auto_tac;
 qed "split_sum_case";
 
+qed_goal "split_sum_case_asm" Sum.thy "P (sum_case f g s) = \
+\ (~((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))"
+    (K [stac split_sum_case 1,
+	Blast_tac 1]);
+
 (*Prevents simplification of f and g: much faster*)
 qed_goal "sum_case_weak_cong" Sum.thy
   "s=t ==> sum_case f g s = sum_case f g t"