Re: [isabelle] defining nat1 in isabelle

Hi Leo, 

You can use the "typedef" command to create new types like this. See

on pages 173-176 for more information.

Best wishes,

On 15 Apr 2013, at 17:39, Leo Freitas wrote:

> Hi,
> I am new to Isabelle and its type ways of declaring / defining new types.
> In particular when extending type classes like say nat1 as an extension of nat (n > 0).
> I couldn't find it in the sources and I wondered if someone has done this already.
> Looking at Nat.thy and Orderings.thy I saw the main aspects of Nat characterisation
> but failed to properly extend my theory to cope with something like nat1.
> Any help / clues is much appreciated.
> Best,
> Leo

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