Re: [isabelle] Specializing types in locales

Thanks Brian and Clemens,

The Brian's solution worked well but it was still necessary to contrains all 

With Clemens' one, it is not any more necessary: the type is constrained once 
for all parameters.

However, is there anyone having a clue about my last question?

> > A great feature would be to have specializable
> > type declarations but I've understood it wasn't possible due to the
> > logical framework (quantification on types) in an email from Makarius:
> >
> > 
> > I know I could also use AWE, but there is no release for Isabelle 2009-2
> > (but I haven't tried the one for Isabelle 2009-2 that could perhaps also
> > work).
> > 
> > Furthermore in an other mail, Makarius said:
> > Trying a bit harder in the internal structures, one could support type
> > parameters on the RHS one day.
> >
> > Is this still a possibility?



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