2016-01-15: Five more theorem prover libraries: Coq, HOL4, TPS, Hol Light, and Isabelle

In the DFG OAF project we build translations from theorem prover libraries to OMDoc/MMT and host them on MathHub for management. We have started working on