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