changeset 56798 | 939e88e79724 |
parent 41561 | d1318f3c86ba |
child 63167 | 0909deb8059b |
56797:32963b43a538 | 56798:939e88e79724 |
---|---|
6 |
6 |
7 theory Hash |
7 theory Hash |
8 imports RMD_Specification |
8 imports RMD_Specification |
9 begin |
9 begin |
10 |
10 |
11 spark_open "rmd/hash.siv" |
11 spark_open "rmd/hash" |
12 |
12 |
13 abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where |
13 abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where |
14 "from_chain c \<equiv> ( |
14 "from_chain c \<equiv> ( |
15 word_of_int (h0 c), |
15 word_of_int (h0 c), |
16 word_of_int (h1 c), |
16 word_of_int (h1 c), |