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:

http://www4.in.tum.de/~berghofe/papers/Poplmark/index.html

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

   Norbert





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