*To*: Christian Sternagel <c.sternagel at gmail.com>*Subject*: Re: [isabelle] type_synonym and fixed type arguments in a locale?*From*: Makarius <makarius at sketis.net>*Date*: Wed, 15 May 2013 11:37:45 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <519309A4.6040003@gmail.com>*References*: <CANofLeKKZZu3n_hrqk1pV4Bhgak2Oa0c30uq33RL8viPCvANbg@mail.gmail.com> <519309A4.6040003@gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 15 May 2013, Christian Sternagel wrote:

* Command 'typedef' now works within a local theory context -- without introducing dependencies on parameters or assumptions, which is not possible in Isabelle/Pure/HOL.

If it would mean that I cannot use locale parameters in the defining setof a typedef, then I would not consider 'typedef' to be localized at all(since the only allowed instances can easily be moved outside the localcontext, or am I missing something?).

Related to Randy's question: is it (or should it, or will it ever be)possible to do the following?locale term_algebra = fixes F :: "'a set" fixes V :: "'b set" begin definition "domain α = {x ∈ V. α x ≠ Var x}" typedef ('a, 'b) subst = "{α :: 'b => ('a, 'b) term. finite (domain α)}" end for which I currently obtain: Locally fixed type arguments "'a", "'b" in type declaration "subst"

Makarius

**References**:**[isabelle] type_synonym and fixed type arguments in a locale?***From:*Randy Pollack

**Re: [isabelle] type_synonym and fixed type arguments in a locale?***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] type_synonym and fixed type arguments in a locale?
- Next by Date: [isabelle] export and import term
- Previous by Thread: Re: [isabelle] type_synonym and fixed type arguments in a locale?
- Next by Thread: Re: [isabelle] type_synonym and fixed type arguments in a locale?
- Cl-isabelle-users May 2013 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