Re: [isabelle] Encoding an evaluation context
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