src/ZF/equalities.ML
changeset 11695 8c66866fb0ff
parent 9907 473a6604da94
child 12199 8213fd95acb5
     1.1 --- a/src/ZF/equalities.ML	Fri Oct 05 16:04:56 2001 +0200
     1.2 +++ b/src/ZF/equalities.ML	Fri Oct 05 21:37:33 2001 +0200
     1.3 @@ -99,19 +99,19 @@
     1.4  
     1.5  (** Simple properties of Diff -- set difference **)
     1.6  
     1.7 -Goal "A-A = 0";
     1.8 +Goal "A - A = 0";
     1.9  by (Blast_tac 1);
    1.10  qed "Diff_cancel";
    1.11  
    1.12 -Goal "0-A = 0";
    1.13 +Goal "0 - A = 0";
    1.14  by (Blast_tac 1);
    1.15  qed "empty_Diff";
    1.16  
    1.17 -Goal "A-0 = A";
    1.18 +Goal "A - 0 = A";
    1.19  by (Blast_tac 1);
    1.20  qed "Diff_0";
    1.21  
    1.22 -Goal "A-B=0 <-> A<=B";
    1.23 +Goal "A - B = 0 <-> A <= B";
    1.24  by (blast_tac (claset() addEs [equalityE]) 1);
    1.25  qed "Diff_eq_0_iff";
    1.26