changeset 56798 | 939e88e79724 |
parent 41561 | d1318f3c86ba |
child 63167 | 0909deb8059b |
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy Tue Apr 29 22:52:15 2014 +0200 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy Wed Apr 30 15:43:44 2014 +0200 @@ -8,7 +8,7 @@ imports RMD_Specification begin -spark_open "rmd/hash.siv" +spark_open "rmd/hash" abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where "from_chain c \<equiv> (