Re: [isabelle] A few questions about Isabelle2013

On Tue, 15 Jan 2013, Gottfried Barrow wrote:

These 5 examples give me an error that I don't get in Isabelle2012:

(* \<...>  *)
  Error: Malformed command syntax

All Isabelle source text needs to conform to the official Isabelle symbol syntax. Isabelle2013 is more thorough in checking that, even inside comments.

--"\<rbrace>", --"\<lbrace>", --{* \<lbrace> *}, and --{* \<rbrace> *}
  Error: Unbalanced antiquotation block parentheses

There was an omission of not observing these formal-comments. This is done in Isabelle2013, so for example

  -- {* look here @{term "λx. x"} *}

will have the proper formal markup for the embedded term inside the antiquotation. \<rbrace> and \<lbrace> are part of the official antiquotation syntax, although they are rarely used. You can evade by inventing referring to funny symbols that are not used elsewhere yet.


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