[isabelle] Imperative HOL
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