src/HOL/ex/LocaleTest2.thy
changeset 29223 e09c53289830
parent 28823 dcbef866c9e2
child 29226 fcc9606fe141
     1.1 --- a/src/HOL/ex/LocaleTest2.thy	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/HOL/ex/LocaleTest2.thy	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -433,8 +433,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -interpretation dlo < dlat
     1.8 -(* TODO: definition syntax is unavailable *)
     1.9 +sublocale dlo < dlat
    1.10  proof
    1.11    fix x y
    1.12    from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
    1.13 @@ -445,7 +444,7 @@
    1.14    then show "EX sup. is_sup x y sup" by blast
    1.15  qed
    1.16  
    1.17 -interpretation dlo < ddlat
    1.18 +sublocale dlo < ddlat
    1.19  proof
    1.20    fix x y z
    1.21    show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")