Subst/ROOT.ML
changeset 8 8dd033c3ffbc
parent 0 7949f97df77a
child 17 8c0c3a67d9e1
--- a/Subst/ROOT.ML	Fri Oct 08 13:46:13 1993 +0100
+++ b/Subst/ROOT.ML	Sun Oct 17 17:23:51 1993 +0100
@@ -14,7 +14,7 @@
 setplus      -  minor additions to HOL's set theory
 alist        -  association lists
 uterm        -  inductive data type of terms
-utermlemmas  -  definition of occurs and vars_of for terms
+utlemmas     -  definition of occurs and vars_of for terms
 subst        -  substitutions
 unifier      -  specification of unification and conditions for 
                 correctness and termination
@@ -29,7 +29,7 @@
 
 use_thy "Subst/alist";
 use_thy "Subst/uterm";
-use_thy "Subst/utermlemmas";
+use_thy "Subst/utlemmas";
 
 use_thy "Subst/subst";
 use_thy "Subst/unifier";