changeset 11695 | 8c66866fb0ff |
parent 11323 | 92eddd0914a9 |
child 12199 | 8213fd95acb5 |
--- a/src/ZF/simpdata.ML Fri Oct 05 16:04:56 2001 +0200 +++ b/src/ZF/simpdata.ML Fri Oct 05 21:37:33 2001 +0200 @@ -54,9 +54,9 @@ "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"] val misc_simps = map prover - ["0 Un A = A", "A Un 0 = A", + ["0 Un A = A", "A Un 0 = A", "0 Int A = 0", "A Int 0 = 0", - "0-A = 0", "A-0 = A", + "0 - A = 0", "A - 0 = A", "Union(0) = 0", "Union(cons(b,A)) = b Un Union(A)", "Inter({b}) = b"]