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