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
> formalizing a
> modeling language for embedded systems.
I'd be interested to see something like that, if you have a reference/link.
This archive was generated by a fusion of
Pipermail (Mailman edition) and