src/HOL/GCD.thy
changeset 32879 7f5ce7af45fd
parent 32479 521cc9bf2958
child 32960 69916a850301
     1.1 --- a/src/HOL/GCD.thy	Mon Oct 05 17:28:59 2009 +0100
     1.2 +++ b/src/HOL/GCD.thy	Tue Oct 06 15:51:34 2009 +0200
     1.3 @@ -1575,7 +1575,7 @@
     1.4  qed
     1.5  
     1.6  interpretation gcd_lcm_complete_lattice_nat:
     1.7 -  complete_lattice "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0 GCD LCM
     1.8 +  complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
     1.9  proof
    1.10    case goal1 show ?case by simp
    1.11  next