# HG changeset patch
# User nipkow
# Date 774273198 -7200
# Node ID 3da472b96f25f43a07b6c80275444f36d13b2b35
# Parent  8bb25bc98a2741ff98006851da657b7cefa54c69
added val eq_sym_conv = prover "(x=y) = (y=x)";

diff -r 8bb25bc98a27 -r 3da472b96f25 simpdata.ML
--- 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))";