equal
deleted
inserted
replaced
7 theory BVExample |
7 theory BVExample |
8 imports |
8 imports |
9 "../JVM/JVMListExample" |
9 "../JVM/JVMListExample" |
10 BVSpecTypeSafe |
10 BVSpecTypeSafe |
11 JVM |
11 JVM |
12 "~~/src/HOL/Library/More_Set" |
|
13 begin |
12 begin |
14 |
13 |
15 text {* |
14 text {* |
16 This theory shows type correctness of the example program in section |
15 This theory shows type correctness of the example program in section |
17 \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by |
16 \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by |