Re: [isabelle] defining nat1 in isabelle
You can use the "typedef" command to create new types like this. See
on pages 173-176 for more information.
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