Re: [isabelle] Encoding an evaluation context

Hello Klaus
On Wednesday 19 April 2006 15:07, Klaus Ostermann wrote:
> What would be a good way to encode an evaluation context in Isabelle? Are
> there maybe existing examples that I could look at?

See for example the work of Stefan Berghofer for the Poplmark-Challenge:

He uses a function E:: term => term to encode evalution contexts.
An inductive definition "ctxt" restricts the E to sensible functions.


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