equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/DFA/Abstract_BV.thy |
1 (* Title: HOL/MicroJava/DFA/Abstract_BV.thy |
2 Author: Gerwin Klein |
2 Author: Gerwin Klein |
3 Copyright 2003 TUM |
3 Copyright 2003 TUM |
4 *) |
4 *) |
5 |
5 |
6 section {* Abstract Bytecode Verifier *} |
6 section \<open>Abstract Bytecode Verifier\<close> |
7 |
7 |
8 (*<*) |
8 (*<*) |
9 theory Abstract_BV |
9 theory Abstract_BV |
10 imports Typing_Framework_err Kildall LBVCorrect LBVComplete |
10 imports Typing_Framework_err Kildall LBVCorrect LBVComplete |
11 begin |
11 begin |