[isabelle] Encoding an evaluation context

Hi there,

I am trying to formalize a programming language semantics.

Small-step semantics are frequently formalized by using an evaluation
context which controls the order of evaluation. 

What would be a good way to encode an evaluation context in Isabelle? Are
there maybe existing examples that I could look at?


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