Fix minor bug caused by lg constant's move from util_prob to transc

Document same in release notes.
HOL-Theorem-Prover · Jul 19, 2023 · 2ee6798 · 2ee6798 · binghe · Jul 19, 2023
1 parent 4ff0a93
commit 2ee6798
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git 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`.
+
 * * * * *
 
 <div class="footer">

diff --git 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