| changeset 58886 | 8a6cac7c7247 |
| parent 42463 | f270e3e18be5 |
| child 61361 | 8b5f00202e1a |
| 58885:47fdd4f40d00 | 58886:8a6cac7c7247 |
|---|---|
1 (* Title: HOL/MicroJava/BV/LBVJVM.thy |
1 (* Title: HOL/MicroJava/BV/LBVJVM.thy |
2 Author: Tobias Nipkow, Gerwin Klein |
2 Author: Tobias Nipkow, Gerwin Klein |
3 Copyright 2000 TUM |
3 Copyright 2000 TUM |
4 *) |
4 *) |
5 |
5 |
6 header {* \isaheader{LBV for the JVM}\label{sec:JVM} *} |
6 section {* LBV for the JVM \label{sec:JVM} *} |
7 |
7 |
8 theory LBVJVM |
8 theory LBVJVM |
9 imports Typing_Framework_JVM |
9 imports Typing_Framework_JVM |
10 begin |
10 begin |
11 |
11 |