1.1 --- a/src/HOL/MicroJava/BV/Semilat.thy	Fri Jun 17 11:35:35 2005 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Semilat.thy	Fri Jun 17 16:12:49 2005 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    \isaheader{Semilattices} 
     1.5  *}
     1.6  
     1.7 -theory Semilat = While_Combinator:
     1.8 +theory Semilat imports While_Combinator begin
     1.9  
    1.10  types 'a ord    = "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.11        'a binop  = "'a \<Rightarrow> 'a \<Rightarrow> 'a"