src/FOLP/IFOLP.thy
changeset 1149 5750eba8820d
parent 1142 eb0e2ff8f032
child 1477 4c51ab632cda
     1.1 --- a/src/FOLP/IFOLP.thy	Wed Jun 21 11:35:10 1995 +0200
     1.2 +++ b/src/FOLP/IFOLP.thy	Wed Jun 21 15:01:07 1995 +0200
     1.3 @@ -84,8 +84,8 @@
     1.4  
     1.5  disjI1    "a:P ==> inl(a):P|Q"
     1.6  disjI2    "b:Q ==> inr(b):P|Q"
     1.7 -disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R \
     1.8 -\          |] ==> when(a,f,g):R"
     1.9 +disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R 
    1.10 +          |] ==> when(a,f,g):R"
    1.11  
    1.12  (* Implication *)
    1.13