Re: [isabelle] Extracting assumptions from an Isar proof
On 16/04/10 08:39, Jasmin Blanchette wrote:
Does anyone know if there's a parser for Isar proofs? In particular,
are there existing ways for extracting the assumptions used in a
particular proof given a .thy file?
I'm not sure I totally understand what you want to do. By assumptions,
do you mean the theorems used in the proof?
Yes, that's right. Can all theorems used in a proof be extracted?
Postal Address: School of Informatics, University of Edinburgh,
Room 2.05, Informatics Forum, 10 Crichton Street,
Edinburgh EH8 9AB, UK.
Telephone Number: +44-131-651-3077,
Fax Number: +44-131-650-6899,
Email: M.Chan at ed.ac.uk.
Web Page: http://homepages.inf.ed.ac.uk/mchan/
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