| changeset 25592 | e8ddaf6bf5df |
| parent 23757 | 087b0a241557 |
| child 27681 | 8cedebf55539 |
--- a/src/HOL/MicroJava/BV/Semilat.thy Mon Dec 10 11:24:03 2007 +0100 +++ b/src/HOL/MicroJava/BV/Semilat.thy Mon Dec 10 11:24:06 2007 +0100 @@ -11,7 +11,9 @@ \isaheader{Semilattices} *} -theory Semilat imports While_Combinator begin +theory Semilat +imports Main While_Combinator +begin types 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"