src/FOL/ROOT.ML
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