equal
deleted
inserted
replaced
3 Author: Stefan Berghofer |
3 Author: Stefan Berghofer |
4 *) |
4 *) |
5 |
5 |
6 header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *} |
6 header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *} |
7 |
7 |
8 theory JVMListExample = SystemClasses + JVMExec: |
8 theory JVMListExample imports SystemClasses JVMExec begin |
9 |
9 |
10 consts |
10 consts |
11 list_nam :: cnam |
11 list_nam :: cnam |
12 test_nam :: cnam |
12 test_nam :: cnam |
13 append_name :: mname |
13 append_name :: mname |