equal
deleted
inserted
replaced
1 (* Title: Substitutions/utermlemmas.thy |
1 (* Title: Substitutions/utermlemmas.thy |
2 Author: Martin Coen, Cambridge University Computer Laboratory |
2 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Copyright 1993 University of Cambridge |
3 Copyright 1993 University of Cambridge |
4 |
4 |
5 Additional definitions for uterms that are not part of the basic inductive definition. |
5 Additional definitions for uterms that are not part of the basic inductive definition. |
6 *) |
6 *) |
7 |
7 |