Re: [isabelle] Trouble with the Int Theory



On 01.11.2014 10:21, Peter Lammich wrote:
> Hi,
> 
> try 
>       note [[ show_sorts]]
>       thm of_int_eq_0_iff
> 
> here, you will see that the of_int_eq_0_iff lemma only works
> if the right hand side is in the ring_char_0 typeclass. 

The same can also be seen without show_sorts by hovering over the
variables in the lemma.

  -- Lars

Attachment: signature.asc
Description: OpenPGP digital signature



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