[isabelle-dev] numeral type translations
makarius at sketis.net
Wed May 30 10:50:46 CEST 2012
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
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
More information about the isabelle-dev