| changeset 44013 | 5cfc1c36ae97 |
| parent 38140 | 05691ad74079 |
| 44012:8c1dfd6c2262 | 44013:5cfc1c36ae97 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Unification Algorithm *} |
6 header {* Unification Algorithm *} |
7 |
7 |
8 theory Unify |
8 theory Unify |
9 imports Unifier |
9 imports Unifier "~~/src/HOL/Library/Old_Recdef" |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Substitution and Unification in Higher-Order Logic. *} |
12 subsection {* Substitution and Unification in Higher-Order Logic. *} |
13 |
13 |
14 text {* |
14 text {* |