In interactive theorem proving HOL4 (http://hol.sourceforge.net/) and Isabelle (http://isabelle.in.tum.de/) are written in SML and are actively developed.