Both are interactive theorem provers, so yeah. But the two school comment said Coq/dependent-types, and Isabelle/HOL is neither Coq, nor does it do dependent ty

Both are interactive theorem provers, so yeah. But the two school comment said Coq/dependent-types, and Isabelle/HOL is neither Coq, nor does it do dependent types :) If you are looking for developments in Isabelle/HOL, there is the AFP: https://www.isa-afp.org/ https://www.isa-afp.org/ There is also a recent book that might interest you: http://www.concrete-semantics.org/ http://www.concrete-semantics.org/