[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?

Regards,
Klaus






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