src/HOL/ROOT.ML
changeset 4320 24d9e6639cd4
parent 4296 aa84d9c62454
child 4517 fad9b7479dbe
     1.1 --- a/src/HOL/ROOT.ML	Fri Nov 28 07:35:47 1997 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Fri Nov 28 07:37:06 1997 +0100
     1.3 @@ -24,6 +24,7 @@
     1.4  use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
     1.5  use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
     1.6  use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
     1.7 +use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
     1.8  
     1.9  use "thy_data.ML";
    1.10