changeset 19783 | 82f365a14960 |
parent 17436 | 4e603046e539 |
child 19931 | fb32b43e7f80 |
--- 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 *}