Re: [isabelle] defining nat1 in isabelle

Hi John,

I think this use of "typedef" is deprecated. Although Isabelle still accepts it, I remember seeing warnings.

All the best,

On 04/16/2013 02:09 PM, John Wickerson wrote:
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:


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.


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