(* Title: HOL/MicroJava/BV/Semilat.thy Author: Gerwin Klein Copyright 2003 TUM *) header {* Abstract Bytecode Verifier *} (*<*) theory Abstract_BV imports Typing_Framework_err Kildall LBVCorrect LBVComplete begin end (*>*)