changeset 4349 | 50403e5a44c0 |
parent 4223 | f60e3d2c81d3 |
child 4466 | 305390f23734 |
--- a/src/FOL/ROOT.ML Wed Dec 03 10:47:13 1997 +0100 +++ b/src/FOL/ROOT.ML Wed Dec 03 10:48:16 1997 +0100 @@ -19,8 +19,10 @@ use "$ISABELLE_HOME/src/Provers/hypsubst.ML"; use "$ISABELLE_HOME/src/Provers/classical.ML"; use "$ISABELLE_HOME/src/Provers/blast.ML"; +use "$ISABELLE_HOME/src/Provers/quantifier1.ML"; use_thy "IFOL"; +use "fologic.ML"; (** Applying HypsubstFun to generate hyp_subst_tac **) structure Hypsubst_Data =