Re: [isabelle] antiquotations

On 06/05/2018 07:53 PM, Makarius wrote:
In Isabelle you have the goal right there in the source,

Hi Makarius,

not clear what you mean by this - sure, the goal has been entered in textual form by the user, and obviously the system turns this into the ML value - but I can't see how the ML value is "there in the source".

What do you mean by this?



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