[isabelle-dev] numeral type translations

[Makarius]

On Wed, 30 May 2012, Brian Huffman wrote:

> Hi Gerwin,
>
> I'm responding also to the development list.

Better than just 2 on the thread, but it all looks like perfectly normal 
isabelle-users material below ...

>
> On Wed, May 30, 2012 at 3:36 AM, Gerwin Klein <gerwin.klein at nicta.com.au> 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.

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.


 	Makarius