equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/datatype_abs_proofs.ML |
1 (* Title: HOL/Tools/datatype_abs_proofs.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer |
3 Author: Stefan Berghofer, TU Muenchen |
4 Copyright 1998 TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 Proofs and defintions independent of concrete representation |
6 Proofs and defintions independent of concrete representation |
7 of datatypes (i.e. requiring only abstract properties such as |
7 of datatypes (i.e. requiring only abstract properties such as |
8 injectivity / distinctness of constructors and induction) |
8 injectivity / distinctness of constructors and induction) |
9 |
9 |