src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
changeset 55818 d8b2f50705d0
parent 41588 9546828c0eb3
child 66453 cc19f7ca2ed6
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_Specification
     7 theory RMD_Specification
     8 imports RMD SPARK
     8 imports RMD "~~/src/HOL/SPARK/SPARK"
     9 begin
     9 begin
    10 
    10 
    11 (* bit operations *)
    11 (* bit operations *)
    12 
    12 
    13 abbreviation rotate_left :: "int \<Rightarrow> int \<Rightarrow> int" where
    13 abbreviation rotate_left :: "int \<Rightarrow> int \<Rightarrow> int" where