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


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.


isabelle-dev mailing list

isabelle-dev mailing list

Reply via email to