Hi Gerwin, I'm responding also to the development list.
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" > > term "7 :: 10 word" > > (shows as 10 word) > > In Isabelle2012, it shows as "word8", i.e. all lengths fire the translation. > Changing the "8 word" on the rhs to word_length8 or something like "num1 bit0 > bit0 bit0" won't fire the translation at all. As you suspected, this has nothing to do with the change in numeral representation. It has only to do with Isabelle's parser. I tested the following example in Isabelle/Pure, using the parse/print translations copied from Library/Numeral_Type.thy: type_synonym eight = 8 translations (type) "eight" <= (type) "8" typ "10" (shows as "eight" in Isabelle2012) If you do "Isabelle > Show Me > Internal Syntax" in PG, then you can see a difference in the "print_rules" section: Isabelle2011-1: ("_NumeralType" "8") -> "\<^type>Temp.eight" Isabelle2012: ("_NumeralType" 8) -> "\<^type>Temp.eight" Note the difference in the quotation marks, which indicate that something is a constant. In Isabelle2012, the rule has a free variable called "8", which matches anything, as you observed. I did a bisection to find the origin of the problem: The first bad revision is: changeset: 46236:ae79f2978a67 user: wenzelm date: Mon Jan 16 21:50:15 2012 +0100 summary: position constraints for numerals enable PIDE markup; Unfortunately I don't know of any workaround to get your syntax translations working again. - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
