[isabelle] proofs about grammars?

Are there any existing proofs about grammars in the libraries or proof archives? I would like to be able to prove that some parsing code accepts strings if and only if they are in some context free language specified by a context free grammar (or possibly even a regular language and a
regular expression).

Tim Newsham

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