| changeset 56798 | 939e88e79724 |
| parent 41561 | d1318f3c86ba |
| child 69605 | a96320074298 |
--- a/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy Tue Apr 29 22:52:15 2014 +0200 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy Wed Apr 30 15:43:44 2014 +0200 @@ -8,7 +8,7 @@ imports RMD_Specification begin -spark_open "rmd/k_r.siv" +spark_open "rmd/k_r" spark_vc function_k_r_6 using assms by (simp add: K'_def)