Re: [isabelle] Isabelle records



On Tuesday 20 Sep 2005 23:44, jdavis27 at uiuc.edu wrote:
> Could someone point me out to a white paper, manual, or some
> other documentation that illustrates the use of Isabelle
> records as defined in HOL\Records.thy?

Section 8.2 in the tutorial has a few (small) examples.

You can also get a good list of theorems for a particular field
using "Find Theorems" (C-c C-f in XEmacs) and providing the name
of one of the fields.

I haven't found many real examples though, for example, the 
abstract syntaxes I've seen normally seem to be modelled with
datatype constructors.

> formalizing a
> modeling language for embedded systems.

I'd be interested to see something like that, if you have a reference/link.

Cheers
Martin





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