The project files for the article `Integrating ADTs in KeY and their Application to History-based reasoning.' The archive contains: The bundled version of KeY, key-2.8.0-exe.jar. The java source code of the project. Isabelle code (Collections. thy). The Isabelle version we use is Isabelle 2020. It can be download from the official website. Several user-defined lemmas that we need when we do the proof (addAll_rule.key) A number of proof files that can be loaded in KeY that verifies the contract for our case study. A document showing the proof settings in KeY. Compare to Version 1.0, this version updates the taclets which uses "find" and "replacewith". The taclet uses these two sentences correspond to a bi-implcation, since the term can appear on both sides of the sequent.