Re: [isabelle] Extracting assumptions from an Isar proof

On 16/04/10 08:39, Jasmin Blanchette wrote:
Dear Michael,

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
Web Page:

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.