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