# HG changeset patch
# User wenzelm
# Date 964955098 -7200
# Node ID 2210dffb9764bf1c2b3bae1f8799d818143a5044
# Parent  b24516d96847a8cec8c4de3b29d44802a0c033c1
added split_bind_asm, bind_splits;

diff -r b24516d96847 -r 2210dffb9764 src/HOL/W0/Maybe.ML
--- a/src/HOL/W0/Maybe.ML	Sun Jul 30 13:03:49 2000 +0200
+++ b/src/HOL/W0/Maybe.ML	Sun Jul 30 13:04:58 2000 +0200
@@ -25,6 +25,13 @@
 qed "split_bind";
 
 Goal
+  "P(res bind f) = (~ (res = Fail & ~ P Fail | (? s. res = Ok s & ~ P(f s))))";
+ by (simp_tac (simpset() addsplits [split_bind]) 1);
+qed "split_bind_asm";
+
+bind_thms ("bind_splits", [split_bind, split_bind_asm]);
+
+Goal
   "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
 by (simp_tac (simpset() addsplits [split_bind]) 1);
 qed "bind_eq_Fail";