The group you are posting to is a Usenet group. Messages posted to this group will make your email address visible to anyone on the Internet.
Your reply message has not been sent.
Your post was successful
Newsgroups: fa.isabelle
From: Tobias Nipkow <nip...@in.tum.de>
Date: Thu, 01 Nov 2012 15:06:22 UTC
Local: Thurs, Nov 1 2012 11:06 am
Subject: 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)
If you want to restrict to a subset of a type wityhout creating a completely new
> for things such as non-negative real vectors. type, you must do that on the formula level with explicit assumptions in your propositions. Tobias
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
| ||||||||||||||