Hi, 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 13b06c6261.
-- Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
