[isabelle] defining nat1 in isabelle


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.