--- a/src/HOL/Library/Lattice_Syntax.thy Wed Jul 22 14:21:52 2009 +0200
+++ b/src/HOL/Library/Lattice_Syntax.thy Wed Jul 22 18:02:10 2009 +0200
@@ -4,16 +4,16 @@
(*<*)
theory Lattice_Syntax
-imports Set
+imports Complete_Lattice
begin
notation
+ top ("\<top>") and
+ bot ("\<bottom>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900) and
- top ("\<top>") and
- bot ("\<bottom>")
+ Sup ("\<Squnion>_" [900] 900)
end
(*>*)
\ No newline at end of file