--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Thu Oct 29 09:59:40 2020 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Thu Oct 29 10:03:03 2020 +0000 @@ -5,7 +5,7 @@ *) theory RMD -imports "HOL-Word.Word" +imports "HOL-Library.Word" begin