src/HOL/ROOT.ML
changeset 16019 0e1405402d53
parent 15359 8bad1f42fec0
child 16483 ace3c2b95353
equal deleted inserted replaced
16018:3e4e077af2e7 16019:0e1405402d53
    14 (*old-style theory syntax*)
    14 (*old-style theory syntax*)
    15 use "thy_syntax.ML";
    15 use "thy_syntax.ML";
    16 
    16 
    17 use "hologic.ML";
    17 use "hologic.ML";
    18 
    18 
    19 use "~~/src/Provers/simplifier.ML";
       
    20 use "~~/src/Provers/splitter.ML";
    19 use "~~/src/Provers/splitter.ML";
    21 use "~~/src/Provers/hypsubst.ML";
    20 use "~~/src/Provers/hypsubst.ML";
    22 use "~~/src/Provers/induct_method.ML";
    21 use "~~/src/Provers/induct_method.ML";
    23 use "~~/src/Provers/make_elim.ML";
    22 use "~~/src/Provers/make_elim.ML";
    24 use "~~/src/Provers/classical.ML";
    23 use "~~/src/Provers/classical.ML";