We verified two versions of the CPS transformation in Isabelle/HOL: one by Plotkin by Danvy and Filinski. We adopted first order abstract syntax so that the formalization is close to that of hand-written proofs and compilers. To simplify treatment of fresh variables introduced by the transformation we introduce parameterized der abstract syntax implemented as a polymorphic datatype. The verification of Danvy and Filinski's transformation requires us to reformulate the transformation in several respects. We also need to consider -equivalence of terms for the verification. To make automatic theorem proving possible to some extent, we reformulate -equivalence as a syntax-directed deductive system.