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

Andreas Schropp schropp at in.tum.de
Fri Aug 26 18:43:57 CEST 2011


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.




More information about the isabelle-dev mailing list