[isabelle] Tutorial on Deep Embeddings

I'm looking for a tutorial (or a good example or well explained description) of
how to go about creating a deep embedding of a language in Isabelle/HOL
particularly with reference to defining notions of subterm replacement
and rewriting.

Any pointers much appreciated.

Louise Dennis

Dr. Louise Dennis,
Department of Computer Science, Room 117, Ashton Building,
University of  Liverpool, Liverpool, L69 3BX,  UK.
http://www.csc.liv.ac.uk/~lad/  phone: +44 151 795 4237

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