Re: [isabelle] Define records in ML?

* Thomas Bleher <bleher at> [2006-11-10 10:19]:
> PS: If anyone is interested, I attached the relevant code.
> ISM_package.thy contains the ML code, SLE66.thy is an example using this
> theory. find_field_Typ is the first function which fails under the new
> record implementation.

Sorry, forgot again...

This time it is attached.


Attachment: ism.tar.gz
Description: Binary data

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