src/HOL/equalities.ML
changeset 4231 a73f5a63f197
parent 4200 5a2cd204f8b4
child 4306 ddbe1a9722ab
     1.1 --- a/src/HOL/equalities.ML	Sat Nov 15 18:41:06 1997 +0100
     1.2 +++ b/src/HOL/equalities.ML	Sun Nov 16 16:18:31 1997 +0100
     1.3 @@ -626,7 +626,8 @@
     1.4       "(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",
     1.5       "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
     1.6       "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
     1.7 -     "(UN x:C. A - B x)    = (A - (INT x:C. B x))"];
     1.8 +     "(UN x:C. A - B x)    = (A - (INT x:C. B x))",
     1.9 +     "(UN x:f``A. B x)     = (UN a:A. B(f a))"];
    1.10  
    1.11  val INT_simps = map prover
    1.12      ["!!C. C ~= {} ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
    1.13 @@ -635,7 +636,8 @@
    1.14       "!!C. C ~= {} ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",
    1.15       "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
    1.16       "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
    1.17 -     "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))"];
    1.18 +     "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",
    1.19 +     "(INT x:f``A. B x)    = (INT a:A. B(f a))"];
    1.20  
    1.21  
    1.22  val ball_simps = map prover