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