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
```