Re: [isabelle] Isabelle2014-RC0: symbol completion in antiquotations



On 07/09/2014 05:27 PM, Makarius wrote:
Note that the problem would be absent, if the traditional quotes were
replaced by the more robust cartouches.  But this is a bit speculative
at the moment.
Does that mean that cartouches for antiquotations will not be part of Isabelle2014? Just for the record: I would like to have

  @{term ‹α something›}

since, as you said, this would avoid some problems with symbol completion.

cheers

chris




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