| changeset 11649 | dfb59b9954a6 |
| parent 11549 | e7265e70fd7c |
| child 11809 | c9ffdd63dd93 |
| 11648:d78a82d112e4 | 11649:dfb59b9954a6 |
|---|---|
1 (* Title: HOL/Induct/Term.thy |
1 (* Title: HOL/Induct/Term.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer, TU Muenchen |
3 Author: Stefan Berghofer, TU Muenchen |
4 Copyright 1998 TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 *) |
5 *) |
6 |
6 |
7 header {* Terms over a given alphabet *} |
7 header {* Terms over a given alphabet *} |
8 |
8 |
9 theory Term = Main: |
9 theory Term = Main: |