diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/ROOT --- a/src/HOL/ROOT Sun Aug 21 06:18:23 2022 +0000 +++ b/src/HOL/ROOT Sun Aug 21 06:18:23 2022 +0000 @@ -74,6 +74,7 @@ Datatype_Records (*data refinements and dependent applications*) AList_Mapping + Code_Abstract_Char Code_Binary_Nat Code_Prolog Code_Real_Approx_By_Float