--- 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
--- 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";