moved the "use" directive
authorpaulson
Thu Mar 02 18:49:13 2006 +0100 (2006-03-02)
changeset 19174df9de25e87b3
parent 19173 fee0e93efa78
child 19175 c6e4b073f6a5
moved the "use" directive
src/HOL/HOL.thy
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/HOL.thy	Thu Mar 02 16:01:06 2006 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Mar 02 18:49:13 2006 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  theory HOL
     1.5  imports CPure
     1.6  uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
     1.7 +    "Tools/res_atpset.ML"
     1.8  
     1.9  begin
    1.10  
    1.11 @@ -1018,11 +1019,15 @@
    1.12      and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+
    1.13  lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover
    1.14  
    1.15 +lemmas conj_ac = conj_commute conj_left_commute conj_assoc
    1.16 +
    1.17  lemma disj_comms:
    1.18    shows disj_commute: "(P|Q) = (Q|P)"
    1.19      and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by iprover+
    1.20  lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by iprover
    1.21  
    1.22 +lemmas disj_ac = disj_commute disj_left_commute disj_assoc
    1.23 +
    1.24  lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by iprover
    1.25  lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by iprover
    1.26  
     2.1 --- a/src/HOL/ROOT.ML	Thu Mar 02 16:01:06 2006 +0100
     2.2 +++ b/src/HOL/ROOT.ML	Thu Mar 02 18:49:13 2006 +0100
     2.3 @@ -31,9 +31,6 @@
     2.4  use "~~/src/Provers/quasi.ML";
     2.5  use "~~/src/Provers/order.ML";
     2.6  
     2.7 -
     2.8 -use "Tools/res_atpset.ML";
     2.9 -
    2.10  with_path "Integ" use_thy "Main";
    2.11  
    2.12  path_add "~~/src/HOL/Library";