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