changeset 2866 | 0a648ebbf6d4 |
parent 2469 | b50b8c0eec01 |
child 3511 | da4dd8b7ced4 |
--- a/src/FOL/ROOT.ML Wed Apr 02 15:14:37 1997 +0200 +++ b/src/FOL/ROOT.ML Wed Apr 02 15:18:21 1997 +0200 @@ -19,9 +19,11 @@ use "../Provers/ind.ML"; use "../Provers/hypsubst.ML"; use "../Provers/classical.ML"; +use "../Provers/blast.ML"; use_thy "IFOL"; +(** Applying HypsubstFun to generate hyp_subst_tac **) structure Hypsubst_Data = struct structure Simplifier = Simplifier