author | ballarin |
Fri, 07 Jul 2006 09:24:05 +0200 | |
changeset 20034 | 28fcbcf49fe5 |
parent 20033 | 2b8dbb637792 |
child 20035 | 80c79876d2de |
--- a/src/FOL/ex/LocaleTest.thy Fri Jul 07 02:12:52 2006 +0200 +++ b/src/FOL/ex/LocaleTest.thy Fri Jul 07 09:24:05 2006 +0200 @@ -54,7 +54,7 @@ assumes hom: "h(x ** y) = h(x) ++ h(y)" (* -Graceful handling of type errors? +FIXME: graceful handling of type errors? locale LY = LT mult (infixl "**" 60) + LT add (binder "++" 55) + var h + assumes "mult(x) == add" *)