We discuss integrating abstract data types (ADTs) in the KeY theorem prover, and how to reason about the correctness of the Java Collection interface using histories. We introduce a new method to model histories logically (using the Isabelle theorem prover), and translate inferred rules to user-defined taclets in KeY to improve reasoning. As a case study, we prove the correctness of complex programs, that involve binary methods and client code that operates on multiple objects. This is an extension of our previous work on "History-based Specification and Verification of Java Collection in KeY".