conj_commute,disj_commute: new

--- a/src/FOL/simpdata.ML	Wed Dec 14 13:03:09 1994 +0100
+++ b/src/FOL/simpdata.ML	Wed Dec 14 16:48:36 1994 +0100
@@ -50,6 +50,9 @@
   "(Q | R) & P <-> Q&P | R&P",
   "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
 
+bind_thm("conj_commute", int_prove_fun "P&Q <-> Q&P");
+bind_thm("disj_commute", int_prove_fun "P|Q <-> Q|P");
+
 (** Conversion into rewrite rules **)
 
 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;