author | krauss |

Thu May 17 22:37:34 2007 +0200 (2007-05-17) | |

changeset 23000 | 6f158bba99e4 |

parent 22999 | c1ce129e6f9c |

child 23001 | 3608f0362a91 |

added pointer to new Unification theory

1.1 --- a/src/HOL/Subst/Unify.thy Thu May 17 22:33:41 2007 +0200 1.2 +++ b/src/HOL/Subst/Unify.thy Thu May 17 22:37:34 2007 +0200 1.3 @@ -10,8 +10,12 @@ 1.4 imports Unifier 1.5 begin 1.6 1.7 -text{* 1.8 -Substitution and Unification in Higher-Order Logic. 1.9 +subsection {* Substitution and Unification in Higher-Order Logic. *} 1.10 + 1.11 +text {* 1.12 +NB: This theory is already quite old. 1.13 +You might want to look at the newer Isar formalization of 1.14 +unification in HOL/ex/Unification.thy. 1.15 1.16 Implements Manna and Waldinger's formalization, with Paulson's simplifications, 1.17 and some new simplifications by Slind.