:: deftheorem defines HP_TAUT HILBERT1:def 12 :
HP_TAUT = CnPos ({} HP-WFF);