src/FOLP/IFOLP.thy

--- a/src/FOLP/IFOLP.thy	Wed Jun 21 11:35:10 1995 +0200
+++ b/src/FOLP/IFOLP.thy	Wed Jun 21 15:01:07 1995 +0200
@@ -84,8 +84,8 @@
 
 disjI1    "a:P ==> inl(a):P|Q"
 disjI2    "b:Q ==> inr(b):P|Q"
-disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R \
-\          |] ==> when(a,f,g):R"
+disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R 
+          |] ==> when(a,f,g):R"
 
 (* Implication *)