src/FOL/ROOT.ML
changeset 5219 924359415f09
parent 4466 305390f23734
child 5310 3e14d6d66dab
equal deleted inserted replaced
5218:1a49756a2e68 5219:924359415f09
    17 use "$ISABELLE_HOME/src/Provers/splitter.ML";
    17 use "$ISABELLE_HOME/src/Provers/splitter.ML";
    18 use "$ISABELLE_HOME/src/Provers/ind.ML";
    18 use "$ISABELLE_HOME/src/Provers/ind.ML";
    19 use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
    19 use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
    20 use "$ISABELLE_HOME/src/Provers/classical.ML";
    20 use "$ISABELLE_HOME/src/Provers/classical.ML";
    21 use "$ISABELLE_HOME/src/Provers/blast.ML";
    21 use "$ISABELLE_HOME/src/Provers/blast.ML";
       
    22 use "$ISABELLE_HOME/src/Provers/clasimp.ML";
    22 use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
    23 use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
    23 
    24 
    24 use_thy "IFOL";
    25 use_thy "IFOL";
    25 use "fologic.ML";
    26 use "fologic.ML";
    26 
    27