Re: [isabelle] Proving with Goal.prove
Since we're on Goal.prove, I'd like to ask a quick question: can it be
used to prove schematic goals? It seems that if the goal is, say, "EX
(f::?'a=>?'b)...", the type of f in concl of the focus becomes "'a=>'b".
So if Goal.prove takes only concl of the focus, it'd be non-schematic.
So it seems like Goal.prove handles schematic goals as non-schematic
ones. Am I missing something here?
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