Re: [isabelle] How to access a locale type parameter in a quotient type definition



Am Mittwoch, den 10.07.2019, 10:13 +0100 schrieb Lawrence Paulson:
> Possibly now is a good time to plug my own paper “Defining functions
> on equivalence classes”, which is available* from my webpage
> (https://www.cl.cam.ac.uk/~lp15/papers/refereed.html). In this I
> outline how one can create quotient constructions quite easily using
> the set-theoretic primitives of Isabelle/HOL. Obviously quotient_type
> is easier to use, but as discussed, it wants to introduce a type and
> there is no reason on earth to conflate quotient constructions with
> types.
> 
> Larry Paulson
> 
> * It is available via an ACM system that supposedly provides open
>   access from the author’s own webpage. If it doesn’t work for you, 
>   please email me for a copy.

Thanks for the pointer!

Unfortunately, I cannot download the paper via that link.

All the best,
Wolfgang





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