*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Defining a function on an inductively defined set.*From*: Bart Kastermans <Bart.Kastermans at Colorado.EDU>*Date*: Tue, 01 Sep 2009 12:07:02 -0600*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

In http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/Finite.html

F : Fin(A) => A.

Best, Bart

**Follow-Ups**:**Re: [isabelle] Defining a function on an inductively defined set.***From:*Tobias Nipkow

**Re: [isabelle] Defining a function on an inductively defined set.***From:*Tobias Nipkow

**Re: [isabelle] Defining a function on an inductively defined set.***From:*Slawomir Kolodynski

- Previous by Date: [isabelle] A basic proof
- Next by Date: [isabelle] Types for variables
- Previous by Thread: [isabelle] A basic proof
- Next by Thread: Re: [isabelle] Defining a function on an inductively defined set.
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list