| changeset 15481 | fc075ae929e4 |
| parent 14981 | e73f8140af78 |
| child 32960 | 69916a850301 |
| 15480:cb3612cc41a3 | 15481:fc075ae929e4 |
|---|---|
1 (* Title: HOL/MicroJava/Comp/TranslCompTp.thy |
1 (* Title: HOL/MicroJava/Comp/TranslCompTp.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin Strecker |
3 Author: Martin Strecker |
4 *) |
4 *) |
5 |
5 |
6 theory TranslCompTp = JVMType + Index: |
6 theory TranslCompTp |
7 imports Index "../BV/JVMType" |
|
8 begin |
|
9 |
|
7 |
10 |
8 |
11 |
9 (**********************************************************************) |
12 (**********************************************************************) |
10 |
13 |
11 |
14 |