equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/DFA/Semilat.thy |
1 (* Title: HOL/MicroJava/DFA/Semilat.thy |
2 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
3 Copyright 2000 TUM |
3 Copyright 2000 TUM |
4 *) |
4 *) |
5 |
5 |
6 header {* |
6 chapter {* Bytecode Verifier \label{cha:bv} *} |
7 \chapter{Bytecode Verifier}\label{cha:bv} |
7 |
8 \isaheader{Semilattices} |
8 section {* Semilattices *} |
9 *} |
|
10 |
9 |
11 theory Semilat |
10 theory Semilat |
12 imports Main "~~/src/HOL/Library/While_Combinator" |
11 imports Main "~~/src/HOL/Library/While_Combinator" |
13 begin |
12 begin |
14 |
13 |