| changeset 11649 | dfb59b9954a6 |
| parent 11046 | b5f5942781a0 |
| child 12171 | dc87f33db447 |
| 11648:d78a82d112e4 | 11649:dfb59b9954a6 |
|---|---|
1 (* Title: HOL/Induct/ABexp.thy |
1 (* Title: HOL/Induct/ABexp.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 {* Arithmetic and boolean expressions *} |
7 header {* Arithmetic and boolean expressions *} |
8 |
8 |
9 theory ABexp = Main: |
9 theory ABexp = Main: |