1.1 --- a/src/HOL/Complete_Lattice.thy	Tue Oct 06 18:27:00 2009 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Tue Oct 06 20:00:08 2009 +0200
     1.3 @@ -15,21 +15,25 @@
     1.4    bot ("\<bottom>")
     1.5  
     1.6  
     1.7 +subsection {* Syntactic infimum and supremum operations *}
     1.8 +
     1.9 +class Inf =
    1.10 +  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    1.11 +
    1.12 +class Sup =
    1.13 +  fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.14 +
    1.15  subsection {* Abstract complete lattices *}
    1.16  
    1.17 -class complete_lattice = lattice + bot + top +
    1.18 -  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    1.19 -    and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.20 +class complete_lattice = lattice + bot + top + Inf + Sup +
    1.21    assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
    1.22       and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
    1.23    assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
    1.24       and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
    1.25  begin
    1.26  
    1.27 -term complete_lattice
    1.28 -
    1.29  lemma dual_complete_lattice:
    1.30 -  "complete_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom> Sup Inf"
    1.31 +  "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    1.32    by (auto intro!: complete_lattice.intro dual_lattice
    1.33      bot.intro top.intro dual_preorder, unfold_locales)
    1.34        (fact bot_least top_greatest

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