Re: [isabelle] Imperative HOL
The Linked List example and the MREC combinator are already since
December 2009 (changeset 1a82e2e29d67) in the development snapshot.
The Sat-checker and the Bytecode-verifier are still in another
repository. If you are interested, we can give you those files.
If you want to continue working on those, i.e. the SAT checker would be
a perfect example for the new Collection framework (e.g. the clauses are
sets implemented by sorted lists at the moment), I would suggest to turn
these files into a new AFP entry.
Happy Easter wishes,
Peter Lammich wrote:
The TPHOL's 08 paper "Imperative Functional Programming with
Isabelle/HOL" describes some features that
are not contained in the Isabelle2009-1 distribution
For example, the datatype definition for a linked list does not work out
of the box,
it gives the error that \alpha node is not in heap-typeclass.
Moreover, there is no implementation of the mentioned MREC-combinator.
Also, I cannot find the described examples (SAT-checker,
Is there a more complete implementation? Is it available? Are the
This archive was generated by a fusion of
Pipermail (Mailman edition) and