Web appendix of the paper

 a Definitional Two Level Approach to Reasoning
with  Higher Order Abstract Syntax.

Amy Felty and Alberto Momigliano.

The Hybrid package has been developed for Coq and Isabelle/HOL

As far as Isabelle/HOL is concerned, the situation is more complicated due to the fact new versions of HOL are not conservative w.r.t. the previous ones and porting theories through versions may be painful. For example the jump from HOL 2005 to 2007 more or less eliminated the tactical language and the interaction with the shell. So the the Isabelle/HOL code will be organized around versions. If the reader feel the need for other files for better understanding we will be happy to post them.