equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/datatype_rep_proofs.ML |
1 (* Title: HOL/Tools/datatype_rep_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 Definitional introduction of datatypes |
6 Definitional introduction of datatypes |
7 Proof of characteristic theorems: |
7 Proof of characteristic theorems: |
8 |
8 |
9 - injectivity of constructors |
9 - injectivity of constructors |