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.
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