Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Now loads blast.ML
authorpaulson
Wed, 02 Apr 1997 15:18:21 +0200
changeset 2866 0a648ebbf6d4
parent 2865 77daca16b2f4
child 2867 0aa5a3cd4550
Now loads blast.ML
src/FOL/ROOT.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle