section ‹RIPEMD-160-SPARK› theory RIPEMD_160_SPARK imports "HOL-SPARK-Examples.F" "HOL-SPARK-Examples.Hash" "HOL-SPARK-Examples.K_L" "HOL-SPARK-Examples.K_R" "HOL-SPARK-Examples.R_L" "HOL-SPARK-Examples.Round" "HOL-SPARK-Examples.R_R" "HOL-SPARK-Examples.S_L" "HOL-SPARK-Examples.S_R" begin text ‹This entry is empty, because the verification of @{term RMD.rmd} is now contained in the Isabelle distibution.› end