On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp <schr...@in.tum.de> wrote: > On 08/26/2011 10:38 PM, Makarius wrote: >> >> What is gained from that apart from having two versions of typedef? > > I am with you here. > We don't need two primitive versions of typedefs.
This is incorrect: Only the predicate-based typedef need be primitive. The set-based typedef can be implemented definitionally as a thin layer on top of the predicate-based one. - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
