Re: [isabelle] Define records in ML?



* Thomas Bleher <bleher at informatik.uni-muenchen.de> [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.

Thomas

Attachment: ism.tar.gz
Description: Binary data



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