[isabelle-dev] Theory for discrete log etc.

[Florian Haftmann]

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

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160813/5bcad582/attachment.asc>