fixed a bug many years old in rule plusEC
authorpaulson
Mon Apr 26 13:25:49 1999 +0200 (1999-04-26)
changeset 65099f7f4fd05b1f
parent 6508 b8a1e395edd7
child 6510 b5ef6d115b45
fixed a bug many years old in rule plusEC
src/FOLP/IFOLP.thy
     1.1 --- a/src/FOLP/IFOLP.thy	Mon Apr 26 10:44:45 1999 +0200
     1.2 +++ b/src/FOLP/IFOLP.thy	Mon Apr 26 13:25:49 1999 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  
     1.5  whenBinl  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
     1.6  whenBinr  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
     1.7 -plusEC    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = p : P|Q"
     1.8 +plusEC    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
     1.9  
    1.10  applyB     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
    1.11  funEC      "f:P ==> f = lam x. f`x : P"