equal
deleted
inserted
replaced
|
1 (* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy |
|
2 ID: $Id$ |
|
3 Author: Cornelia Pusch |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 |
|
6 Proof that the specification of the bytecode verifier only admits type safe |
|
7 programs. |
|
8 *) |
|
9 |
|
10 BVSpecTypeSafe = Correct |