*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Specification depends on extra type variables*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Mon, 29 Mar 2010 20:53:37 +0300*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <cc2478ab1003270804q6b33d897q4192817c153a56f3@mail.gmail.com>*References*: <4BAB71A4.1020204@uibk.ac.at> <4BAC7B81.5090401@in.tum.de> <4BACAD70.4090409@abo.fi> <cc2478ab1003270804q6b33d897q4192817c153a56f3@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 6.1; en-US; rv:1.9.1.8) Gecko/20100227 Thunderbird/3.0.3

Hello Brian,

(pair) and I fixed that in the locale too.

need is an existential quantification on the extra type: axioms f_def2: "f (a::'a) = (EX 'b::type . (EX (g::'b => 'a). inj g))"

would allow something similar to this? Viorel

If you really want to avoid explicitly passing around an extra dummy parameter, here's what I would recommend: Declare a locale that fixes the dummy type parameter of type "'b itself", and define your constants (which may refer to the locally-fixed type 'b) inside the locale. - Brian

**References**:**[isabelle] Antiquotation for Theorem Names***From:*Christian Sternagel

**Re: [isabelle] Antiquotation for Theorem Names***From:*Alexander Krauss

**[isabelle] Specification depends on extra type variables***From:*Viorel Preoteasa

**Re: [isabelle] Specification depends on extra type variables***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Announcing I3P
- Next by Date: [isabelle] about I3P
- Previous by Thread: Re: [isabelle] Specification depends on extra type variables
- Next by Thread: [isabelle] Antiqutation for Theorem names
- Cl-isabelle-users March 2010 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