src/HOL/ROOT.ML
changeset 4296 aa84d9c62454
parent 4222 d7573d6d0513
child 4320 24d9e6639cd4
     1.1 --- a/src/HOL/ROOT.ML	Wed Nov 26 16:44:25 1997 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Wed Nov 26 16:44:47 1997 +0100
     1.3 @@ -21,7 +21,9 @@
     1.4  use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
     1.5  use "$ISABELLE_HOME/src/Provers/classical.ML";
     1.6  use "$ISABELLE_HOME/src/Provers/blast.ML";
     1.7 -use "$ISABELLE_HOME/src/Provers/nat_transitive.ML";
     1.8 +use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
     1.9 +use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
    1.10 +use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
    1.11  
    1.12  use "thy_data.ML";
    1.13  
    1.14 @@ -37,6 +39,9 @@
    1.15  use_thy "Gfp";
    1.16  
    1.17  use "datatype.ML";
    1.18 +use_thy "Arith";
    1.19 +use "arith_data.ML";
    1.20 +
    1.21  use "ind_syntax.ML";
    1.22  use "add_ind_def.ML";
    1.23  use_thy "intr_elim";