As Alex Nelson pointed out, I think this is exactly the LCF approach to theorem proving. See The LCF Approach
to Theorem Proving for details.
HOL-Light would certainly fit this description. You literally use HOL-Light inside OCaml. (Back when I coded in HOL-Light, I would code up my proof in an editor and paste it into an OCaml interpreter.) You can get a flavor by looking at the HOL Light code. For example, here is a theorem in HOL Light:
let ARITHMETIC_PROGRESSION_LEMMA = prove
(`!n. nsum(0..n) (\i. a + d * i) = ((n + 1) * (2 * a + n * d)) DIV 2`,
INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
prove takes two arguments, the goal to prove, and a tactic to prove that statement (which is usually a number of tactics changed together with the
THEN tactical), and it outputs a theorem. Tactics are just OCaml functions of type
goal -> goalstate. (There is also some tooling in HOL-Light to make it more interactive, but that also is just an OCaml DSL used inside the OCaml REPL.)
If I am not mistaken, the ML family of languages were originally designed exactly to be the Meta Language for LCF provers to implement tactics. From Wikipedia:
Historically, ML was conceived to develop proof tactics in the LCF theorem prover (whose language, pplambda, a combination of the first-order predicate calculus and the simply-typed polymorphic lambda calculus, had ML as its metalanguage).