changeset 81713 | 378b9d6c52b2 |
parent 81642 | e77e8ef5bf9b |
child 81714 | 5e3dd01a9eb2 |
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Sat Jan 04 14:25:56 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Sat Jan 04 14:41:30 2025 +0100 @@ -5,6 +5,7 @@ theory Code_Test_PolyML imports + "HOL-Library.Code_Target_Bit_Shifts" "HOL-Library.Code_Test" Code_Lazy_Test begin