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