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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
