changeset 37744 | 3daaf23b9ab4 |
parent 37165 | c2e27ae53c2a |
child 39557 | fe5722fce758 |
37743:0a3fa8fbcdc5 | 37744:3daaf23b9ab4 |
---|---|
1 (* Title: HOLCF/Tools/domain/domain_take_proofs.ML |
1 (* Title: HOLCF/Tools/Domain/domain_take_proofs.ML |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 |
3 |
4 Defines take functions for the given domain equation |
4 Defines take functions for the given domain equation |
5 and proves related theorems. |
5 and proves related theorems. |
6 *) |
6 *) |