avoid relying on "Thm.definitionK" to pick up definitions -- this was an old hack related to locales (to avoid expanding locale constants to their low-level definition) that is no longer necessary
(* Title: HOL/MicroJava/DFA/Semilattices.thy
Author: Gerwin Klein
Copyright 2003 TUM
*)
header {* Semilattices *}
(*<*)
theory Semilattices
imports Err Opt Product Listn
begin
end
(*>*)