(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy ID: $Id$ Author: Cornelia Pusch Copyright 1999 Technische Universitaet Muenchen Proof that the specification of the bytecode verifier only admits type safe programs. *) BVSpecTypeSafe = Correct