# HG changeset patch
# User wenzelm
# Date 1002310653 -7200
# Node ID 8c66866fb0fff7515a4d204e69c64f076d803c22
# Parent  4c6e9d800628453901d38a97b0e66aeb1a807c03
sane spacing of "-";

diff -r 4c6e9d800628 -r 8c66866fb0ff src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Fri Oct 05 16:04:56 2001 +0200
+++ b/src/ZF/equalities.ML	Fri Oct 05 21:37:33 2001 +0200
@@ -99,19 +99,19 @@
 
 (** Simple properties of Diff -- set difference **)
 
-Goal "A-A = 0";
+Goal "A - A = 0";
 by (Blast_tac 1);
 qed "Diff_cancel";
 
-Goal "0-A = 0";
+Goal "0 - A = 0";
 by (Blast_tac 1);
 qed "empty_Diff";
 
-Goal "A-0 = A";
+Goal "A - 0 = A";
 by (Blast_tac 1);
 qed "Diff_0";
 
-Goal "A-B=0 <-> A<=B";
+Goal "A - B = 0 <-> A <= B";
 by (blast_tac (claset() addEs [equalityE]) 1);
 qed "Diff_eq_0_iff";
 
diff -r 4c6e9d800628 -r 8c66866fb0ff src/ZF/simpdata.ML
--- 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"]