[isabelle] Extracting assumptions from an Isar proof

Hi all,

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


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