In the talk we present InterACT - an interactive theorem prover for conditional equations developed at TU Berlin and used in teaching. First we recapitulate briefly the basics of algebraic specifications. Especially we discuss the inference rules for conditional equations that constitute the theoretical background of InterACT. The second part is devoted for the practical demonstration of the tool. We show the implementation of the inference calculus and demonstrate some nice features of InterACT as, e.g., interactive proof trees and generation of lemmata. We close with some remarks concerning our experience in using InterACT for teaching purposes.