src/FOL/ex/LocaleTest.thy

--- a/src/FOL/ex/LocaleTest.thy	Tue Jun 06 09:28:24 2006 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Tue Jun 06 10:05:57 2006 +0200
@@ -53,8 +53,16 @@
 locale LU = LT mult (infixl "**" 60) + LT add (infixl "++" 55) + var h +
   assumes hom: "h(x ** y) = h(x) ++ h(y)"
 
+(*
+Graceful handling of type errors?
+locale LY = LT mult (infixl "**" 60) + LT add (binder "++" 55) + var h +
+  assumes "mult(x) == add"
+*)
+
 locale LV = LU _ add
 
+locale LW = LU _ mult (infixl "**" 60)
+
 
 subsection {* Constrains *}