Re: [isabelle] antiquotations



On 05/06/18 16:49, Jeremy Dawson wrote:
> 
> On 06/05/2018 07:53 PM, Makarius wrote:
>> In Isabelle you have the goal right there in the source,
> 
> 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?

The true proof state is the partial proof text that you edit in the
Prover IDE: as Isar source.

You don't need the ML value to do the proof, it is part of the
implementation.

It might be fun to explore the implementation, but it can also take some
years to get to the bottom of it.


	Makarius




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