# HG changeset patch
# User lcp
# Date 787420116 -3600
# Node ID b5adfdad06634ef7c6c11052740dc67492cf1bdd
# Parent  08f1785a4384ec336b88f4315dca58a176fe6fc1
conj_commute,disj_commute: new

diff -r 08f1785a4384 -r b5adfdad0663 src/FOL/simpdata.ML
--- 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;