equal
deleted
inserted
replaced
1 (* Title: HOL/Subst/ROOT.ML |
1 (* Title: HOL/Subst/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Substitution and Unification in Higher-Order Logic. |
6 Substitution and Unification in Higher-Order Logic. |
7 |
7 |
8 Implements Manna & Waldinger's formalization, with Paulson's simplifications: |
8 Implements Manna & Waldinger's formalization, with Paulson's simplifications: |