simpdata.ML

 
 val meta_obj_reflection = prove_goal HOL.thy "x==y ==> x=y"
   (fn [prem] => [rewtac prem, rtac refl 1]);
 
 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))";
 val conj_comms = [conj_commute, conj_left_commute];