src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy
changeset 55818 d8b2f50705d0
parent 41587 e13df75fee79
child 62390 842917225d56
equal deleted inserted replaced
55817:0bc0217387a5 55818:d8b2f50705d0
     3 
     3 
     4 Verification of the RIPEMD-160 hash function
     4 Verification of the RIPEMD-160 hash function
     5 *)
     5 *)
     6 
     6 
     7 theory RMD
     7 theory RMD
     8 imports Word
     8 imports "~~/src/HOL/Word/Word"
     9 begin
     9 begin
    10 
    10 
    11 
    11 
    12 (* all operations are defined on 32-bit words *)
    12 (* all operations are defined on 32-bit words *)
    13 
    13