[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

Brian Huffman brianh at cs.pdx.edu
Fri Aug 26 19:13:34 CEST 2011

On Fri, Aug 26, 2011 at 9:43 AM, Andreas Schropp <schropp at in.tum.de> wrote:
> On 08/26/2011 07:02 PM, Brian Huffman wrote:
>> I didn't suggest the idea merely for your benefit. I think this
>> approach would give Isabelle a nicer, simpler logical foundation.
> What is this logical foundation of Isabelle that you have in mind?
> AFAIK I am the only trying to provide a semantics of any kind,
> so please don't think me rude.

I just think that having fewer primitive concepts and fewer axioms is
generally preferable, that is all.

More information about the isabelle-dev mailing list