Re: [isabelle] Proving with Goal.prove

Does the value prop not contain the goal of lem1? If not, how can the
goal for the current goal state be retrieved?


I'm not sure myself, but it seems like the prop here is:

EX (x::'a) y::'a. y < x ==> (EX (x::'a) y::'a. y < x)

so that doesn't look like the goal in lem1. Hopefully someone more familiar with the ML level can answer your question.


Thanks again!


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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