1. [theorem proving] A language in which proofs are

manipulated and tactics are programmed, as opposed to the

logic itself (the "object language"). The first ML was

the metalanguage for the Edinburgh LCF proof assistant.