| 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"