[isabelle] Scan reference
I want to understand the hoare_tac.ML (to customize it). the vcg
method is setup at the end of the linked file
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
my next question is, if there is a reference (or someone can explain
me) the SIMPLE_METHOD' construct.
This archive was generated by a fusion of
Pipermail (Mailman edition) and