[isabelle-dev] Theory for discrete log etc.

[Manuel Eberl]

There's also natlog2 in src/HOL/Analysis/Summation_Tests.thy, which I 
introduced because I didn't know about the other ones.

Manuel


On 13/08/16 15:09, Florian Haftmann wrote:
> Hi all,
>
> after studying 28d1deca302e I realized that we have now two theories
> dealing with discrete functions (with one having been hidden in
> Float.thy for years):
>
>   Log_Nat.floorlog :: "nat ⇒ nat ⇒ nat"
>   Discrete.log :: "nat ⇒ nat"
>   Log_Nat.bitlen :: "int ⇒ int"
>   Discrete.sqrt :: "nat ⇒ nat"
>
> »Discrete.log« seems to be »Log_Nat.floorlog 2« and »Log_Nat.bitlen« is
> just a variant with different types.
>
> Just to place a memo for future consolidation.
>
> Cheers,
> 	Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>