equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/JVM/JVMListExample.thy |
1 (* Title: HOL/MicroJava/JVM/JVMListExample.thy |
2 Author: Stefan Berghofer |
2 Author: Stefan Berghofer |
3 *) |
3 *) |
4 |
4 |
5 header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *} |
5 section {* Example for generating executable code from JVM semantics \label{sec:JVMListExample} *} |
6 |
6 |
7 theory JVMListExample |
7 theory JVMListExample |
8 imports "../J/SystemClasses" JVMExec |
8 imports "../J/SystemClasses" JVMExec |
9 begin |
9 begin |
10 |
10 |