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
> 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and