merged

--- a/src/HOL/Complete_Lattice.thy	Tue Oct 06 18:27:00 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy	Tue Oct 06 20:00:08 2009 +0200
@@ -15,21 +15,25 @@
   bot ("\<bottom>")
 
 
+subsection {* Syntactic infimum and supremum operations *}
+
+class Inf =
+  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
+
+class Sup =
+  fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
+
 subsection {* Abstract complete lattices *}
 
-class complete_lattice = lattice + bot + top +
-  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
-    and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
+class complete_lattice = lattice + bot + top + Inf + Sup +
   assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
      and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
   assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
      and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
 begin
 
-term complete_lattice
-
 lemma dual_complete_lattice:
-  "complete_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom> Sup Inf"
+  "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
   by (auto intro!: complete_lattice.intro dual_lattice
     bot.intro top.intro dual_preorder, unfold_locales)
       (fact bot_least top_greatest

--- a/src/HOL/GCD.thy	Tue Oct 06 18:27:00 2009 +0200
+++ b/src/HOL/GCD.thy	Tue Oct 06 20:00:08 2009 +0200
@@ -1575,7 +1575,7 @@
 qed
 
 interpretation gcd_lcm_complete_lattice_nat:
-  complete_lattice "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0 GCD LCM
+  complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
 proof
   case goal1 show ?case by simp
 next