equal
deleted
inserted
replaced
6 chapter \<open>Bytecode Verifier \label{cha:bv}\<close> |
6 chapter \<open>Bytecode Verifier \label{cha:bv}\<close> |
7 |
7 |
8 section \<open>Semilattices\<close> |
8 section \<open>Semilattices\<close> |
9 |
9 |
10 theory Semilat |
10 theory Semilat |
11 imports Main "~~/src/HOL/Library/While_Combinator" |
11 imports Main "HOL-Library.While_Combinator" |
12 begin |
12 begin |
13 |
13 |
14 type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
14 type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
15 type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
15 type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
16 type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop" |
16 type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop" |