Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions



Am 31/10/2012 19:28, schrieb Christoph LANGE:
> * It would be nice to be able to introduce proper types (not just type_synonyms)
> for things such as non-negative real vectors.

If you want to restrict to a subset of a type wityhout creating a completely new
type, you must do that on the formula level with explicit assumptions in your
propositions.

Tobias





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