On 30/05/2012, at 6:50 PM, Makarius wrote: >> On Wed, May 30, 2012 at 3:36 AM, Gerwin Klein <[email protected]> >> wrote: >>> Hi Brian, >>> >>> not sure if this has anything to do with your change in numerals, but the >>> following used to work as expected in Isabelle2011-1: >>> >>> type_synonym word_length8 = 8 >>> type_synonym word8 = "word_length8 word" >>> translations (type) "word8" <= (type) "8 word" > > Such backward translations of the "type" category have always been fragile > and and the risk of the user, ever since David von Oheimb started these > things in Bali, from where Gerwin has probably picked it up many years ago. > > To ensure that "8" is treated as a syntax constant in Isabelle2012, the usual > way is this: > > syntax "8" :: _ > > I can't say on the spot if it has dire effects on other syntax, though.
Hm, subtle side effects is exactly what I was trying to avoid. In this case, it won't hurt to just not have the translation. > If it does not work, one can use the ML function for translations > (Syntax.update_trrules) to make an Ast pattern where the desired numerals are > Ast.Constant, not Ast.Variable as guessed by the concrete syntax parser. That'll work. Not worth the investment for this one, though. Gerwin _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
