From 2ee6798b66989b9d28b236f460bf6f7f924a84d6 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Wed, 19 Jul 2023 10:51:38 +1000 Subject: [PATCH] Fix minor bug caused by lg constant's move from util_prob to transc Document same in release notes. --- doc/next-release.md | 2 ++ examples/computability/kolmog/kraft_ineqScript.sml | 2 ++ 2 files changed, 4 insertions(+) diff --git a/doc/next-release.md b/doc/next-release.md index 3c8c5237d7..b136fdefb3 100644 --- a/doc/next-release.md +++ b/doc/next-release.md @@ -200,6 +200,8 @@ Incompatibilities: `suminf_def` to reflect its overloading to `suminf`. (All these definitions are generalized versions of those in `seqTheory`.) +* The constant `lg` (logarithm with base 2) has moved from the `util_prob` theory to `transc`. + * * * * *
diff --git a/examples/computability/kolmog/kraft_ineqScript.sml b/examples/computability/kolmog/kraft_ineqScript.sml index 25b9316efa..90ad731fbf 100644 --- a/examples/computability/kolmog/kraft_ineqScript.sml +++ b/examples/computability/kolmog/kraft_ineqScript.sml @@ -20,6 +20,8 @@ val _ = new_theory "kraft_ineq"; val _ = intLib.deprecate_int() +val _ = hide "lg" (* transc$lg is now log base 2 *) + Theorem bool_list_card[simp]: CARD {s | LENGTH (s:bool list) = n} = 2**n Proof