Re: [isabelle] defining nat1 in isabelle



Hi Leo, 

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

http://isabelle.in.tum.de/dist/Isabelle2013/doc/tutorial.pdf

on pages 173-176 for more information.

Best wishes,
John

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.