# HG changeset patch
# User ballarin
# Date 1194281297 -3600
# Node ID 25029ee0a37b8f33e81899c4e61bc2bc85949c8a
# Parent  c532fd8445a2c19f734c98c530c1896f7355d59d
Interpretation with named equations.

diff -r c532fd8445a2 -r 25029ee0a37b src/HOL/ex/LocaleTest2.thy
--- 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