A first order unification algorithm is formalized and proved in this
directory. The files "ROOT.ML" and "ROOT1.ML" give instructions for
running the proof. "ROOT1.ML" is will run on the current Isabelle release
"Isabelle-94 revision 5: January 96"
while "ROOT.ML" builds on an internal release that Carsten Clasholm was
maintaining. Features of this internal release will make their way into
the public release (I hope). Eventually, the definition facility used to
define the Unify algorithm will be incorporated into the syntax for
".thy" files.