[isabelle-dev] Error highlighting in ML for @{lemma}

Lars Noschinski noschinl at in.tum.de
Sat Jun 28 07:57:00 CEST 2014


If I insert a lemma antiquotation in ML code with a proposition with a
type error, the error message is not attached to the proposition or the
antiquotation but to the whole block or file of ML. This refers to

  -- Lars

More information about the isabelle-dev mailing list