Re: [isabelle] Scan reference



Hi Nils,

there is the Isabelle Cookbook, a tutorial for programming Isabelle at the ML level, from the Isabelle documentation project at:

http://isabelle.in.tum.de/nominal/activities/idp/

It explains what Scan and SIMPLE_METHOD are good for and how they are typically used.

Hope this helps,
Andreas

Nils Jähnig schrieb:
Hi,

I want to understand the hoare_tac.ML (to customize it). the vcg
method is setup at the end of the linked file

http://isabelle.in.tum.de/library/HOL/Hoare/Hoare_Logic.html

and it uses the Scan struct (somehow a parser). is there a
documentation/reference for this Scan? i only found several theories
using it for 'method_setup', and in none of the manuals.
i found something called scan.ML in src/HOL/Import, and there is a
function called succeed (as in the call in the file above) in line
117, but it takes two arguments, whereas in the call there is only one
argument.

my next question is, if there is a reference (or someone can explain
me) the SIMPLE_METHOD' construct.


Best Regards
Nils



--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.