src/HOL/HOL.thy
changeset 19174 df9de25e87b3
parent 19162 67436e2a16df
child 19233 77ca20b0ed77
--- a/src/HOL/HOL.thy	Thu Mar 02 16:01:06 2006 +0100
+++ b/src/HOL/HOL.thy	Thu Mar 02 18:49:13 2006 +0100
@@ -8,6 +8,7 @@
 theory HOL
 imports CPure
 uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
+    "Tools/res_atpset.ML"
 
 begin
 
@@ -1018,11 +1019,15 @@
     and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+
 lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover
 
+lemmas conj_ac = conj_commute conj_left_commute conj_assoc
+
 lemma disj_comms:
   shows disj_commute: "(P|Q) = (Q|P)"
     and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by iprover+
 lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by iprover
 
+lemmas disj_ac = disj_commute disj_left_commute disj_assoc
+
 lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by iprover
 lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by iprover