Re: [isabelle] primrec on nested mutually-recursive datatype



Greg Bronevetsky wrote:
Ah, that worked! One final question then. You suggested that I look at the theorem AppSrcStmt_AppSrcOp.size. How do I do that?

Simply use the command

thm AppSrcStmt_AppSrcOp.size

You can use this command inside a theory file, or enter it in the
minibuffer which opens after pressing the "Command" button in the
toolbar of ProofGeneral.

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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