Can someone who knows what a Hilbert calculus is write a tag description for Hilbert-calculus? There's been too recent real analysis/functional analysis/hilbert space questions which have used this tag(assumedly incorrectly).

I have reposted this message in the main chatroom, too, maybe somebody will notice it: chat.stackexchange.com/transcript/message/24278879#24278879