src/FOLP/IFOLP.thy
changeset 1149 5750eba8820d
parent 1142 eb0e2ff8f032
child 1477 4c51ab632cda
--- 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 *)