[NTG-context] old style factorial symbol and theorems