[isabelle] \<fh> as identifier



Hello all,

according to the Isabelle reference manual, identifiers may consist not only of characters and numbers, but also of letters of the form "\<...>" where ... is one letter or two letters. This works well for e.g. \<f> and \<ff>, but if the two letters are different, say \<fh>, then I get an inner lexical syntax error, e.g. in:

term "%\<fh>. 0"

term "%\<f>. 0" and term "%\<ff>. 0" however work perfectly.

How can I use e.g. \<fh> as an identifier in a lambda abstraction?

Thanks in advance,
Andreas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.