changeset 69605 | a96320074298 |
parent 56798 | 939e88e79724 |
--- a/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy Sun Jan 06 15:04:34 2019 +0100 @@ -8,7 +8,7 @@ imports RMD_Specification begin -spark_open "rmd/k_r" +spark_open \<open>rmd/k_r\<close> spark_vc function_k_r_6 using assms by (simp add: K'_def)