src/ZF/simpdata.ML
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"]