src/HOL/ROOT.ML
changeset 15103 79846e8792eb
parent 14398 c5c47703f763
child 15351 bdcd0f321df0
     1.1 --- a/src/HOL/ROOT.ML	Tue Aug 03 13:48:00 2004 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Tue Aug 03 14:47:51 2004 +0200
     1.3 @@ -34,6 +34,7 @@
     1.4  use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
     1.5  use "~~/src/Provers/Arith/extract_common_term.ML";
     1.6  use "~~/src/Provers/Arith/cancel_div_mod.ML";
     1.7 +use "~~/src/Provers/quasi.ML";
     1.8  use "~~/src/Provers/order.ML";
     1.9  
    1.10  with_path "Integ" use_thy "Main";