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