# HG changeset patch
# User paulson
# Date 1141321753 -3600
# Node ID df9de25e87b3845c671e0ab600deee7baf945730
# Parent  fee0e93efa782545f27341f33baee54ff078a2f0
moved the "use" directive

diff -r fee0e93efa78 -r df9de25e87b3 src/HOL/HOL.thy
--- 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
 
diff -r fee0e93efa78 -r df9de25e87b3 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Thu Mar 02 16:01:06 2006 +0100
+++ b/src/HOL/ROOT.ML	Thu Mar 02 18:49:13 2006 +0100
@@ -31,9 +31,6 @@
 use "~~/src/Provers/quasi.ML";
 use "~~/src/Provers/order.ML";
 
-
-use "Tools/res_atpset.ML";
-
 with_path "Integ" use_thy "Main";
 
 path_add "~~/src/HOL/Library";