added val eq_sym_conv = prover "(x=y) = (y=x)";

--- a/simpdata.ML	Tue Jul 12 16:34:45 1994 +0200
+++ b/simpdata.ML	Fri Jul 15 13:53:18 1994 +0200
@@ -68,6 +68,8 @@
 
 in
 
+val eq_sym_conv = prover "(x=y) = (y=x)";
+
 val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
 val conj_commute = prover "(P&Q) = (Q&P)";
 val conj_left_commute = prover "(P&(Q&R)) = (Q&(P&R))";