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?

Cheers,

Jeremy




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