Interpretation with named equations.

--- a/src/HOL/ex/LocaleTest2.thy	Mon Nov 05 17:48:04 2007 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Mon Nov 05 17:48:17 2007 +0100
@@ -490,8 +490,8 @@
   apply (rule int.abs_test) done
 
 interpretation int: dlat ["op <= :: [int, int] => bool"]
-  where "dlat.meet (op <=) (x::int) y = min x y"
-    and "dlat.join (op <=) (x::int) y = max x y"
+  where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
+    and join_eq: "dlat.join (op <=) (x::int) y = max x y"
 proof -
   show "dlat (op <= :: [int, int] => bool)"
     apply unfold_locales