src/HOL/MicroJava/BV/Semilat.thy
changeset 13365 a2c4faad4d35
parent 13077 c2e4d9990162
child 13649 0f562a70c07d
--- a/src/HOL/MicroJava/BV/Semilat.thy	Tue Jul 16 18:25:48 2002 +0200
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Tue Jul 16 18:26:09 2002 +0200
@@ -63,7 +63,7 @@
  some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
 "some_lub r x y == SOME z. is_lub r x y z";
 
-locale semilat =
+locale (open) semilat =
   fixes A :: "'a set"
     and r :: "'a ord"
     and f :: "'a binop"