equal
deleted
inserted
replaced
9 header {* |
9 header {* |
10 \chapter{Bytecode Verifier}\label{cha:bv} |
10 \chapter{Bytecode Verifier}\label{cha:bv} |
11 \isaheader{Semilattices} |
11 \isaheader{Semilattices} |
12 *} |
12 *} |
13 |
13 |
14 theory Semilat imports While_Combinator begin |
14 theory Semilat |
|
15 imports Main While_Combinator |
|
16 begin |
15 |
17 |
16 types 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
18 types 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
17 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
19 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
18 'a sl = "'a set * 'a ord * 'a binop" |
20 'a sl = "'a set * 'a ord * 'a binop" |
19 |
21 |