Theory RIPEMD_160_SPARK

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