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?

Thanks
Michael

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