Re: [isabelle] Isabelle records



If you just want to learn how to use them, how about:
isabelle/HOL/ex/Records.thy

Or would you like something more specific?

Sincerely,

Rafal Kolanski.


jdavis27 at uiuc.edu wrote:
Hello,

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?  While the definition
is clear enough, it would be useful to see a concrete example
that I could relate to my own work, e.g. formalizing a
modeling language for embedded systems.

Thank you for your help,

Justin S. Davis
Graduate student, CS at UIUC





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