equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/TFL/dcterm.ML |
1 (* Title: HOL/Tools/TFL/dcterm.ML |
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
2 Author: Konrad Slind, Cambridge University Computer Laboratory |
4 Copyright 1997 University of Cambridge |
|
5 *) |
3 *) |
6 |
4 |
7 (*--------------------------------------------------------------------------- |
5 (*--------------------------------------------------------------------------- |
8 * Derived efficient cterm destructors. |
6 * Derived efficient cterm destructors. |
9 *---------------------------------------------------------------------------*) |
7 *---------------------------------------------------------------------------*) |