HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism