There is a variety of systems for Interactive Theorem Proving (ITP) -- see also the conference of that name -- Coq, Isabelle, HOLs, ACL2, PVS etc.
All of them are relatively challenging to learn, and each has its own specific culture. It is like learning a foreign language: lets say you know English already, and then have the choice of French, German, Italian, Spanish, Portuguese. All of them are somehow related -- this is not Chinese -- but very few people manage all of that simultaneously. So you should try get a taste for each of the cultures and communities, and then make a commitment.
There might be also the "killer feature" that you really need for your work.
It also helps to have fellow experts on one of these systems around.
- What are the differences between Coq and Isabelle?
Both are descendants of the LCF system from Stanford/Edinburgh/Cambridge. In 1985, G. Huet and L. Paulson were working together on the last version of Cambridge LCF. Then the split happened towards Coc/CIC/COQ (now Coq) in France, and Isabelle in Cambridge and Munich. Note that HOL4, HOL-Light, HOL-XYZ are other related descendants of LCF.
More than 20 years ago, the distinction of Coq vs. Isabelle would have been made according to logical foundations: Dependently Typed Constructive Logic here, Simpl-Typed Classical Logic there. Today, there is surprisingly little impact on that in practice, since more and more layers have been added on top of each formal system, including add-on tools, and libraries.
- Should I learn either Isabelle or Coq, or both?
You should look at both, and try to get a feeling if you like more Wine and Cheese, or Bratwurst and Sauerkraut. (As one of the guys behind Isabelle, but presently at France, I am surprised how many Frenchmen actually like Sauerkraut when they are privately at home and nobody looking :-)
- Is there an advantage to learning either Isabelle or Coq first?
I don't think so. There might be a danger that you get stuck with the one you try first and don't try the second, or that you get disappointed
too early with the first and dismiss it too early. In any case, you will need time and persistence to become productive with either system.
Since Proof General as "IDE" was mentioned already: Proof General / Emacs used to be the standard unifying interface for both Coq and Isabelle over many years, but I would never have called it an IDE. There is also CoqIDE with "IDE" in its name, but is a relatively basic editor on top of Gtk widgets. Current Isabelle includes Isabelle/jEdit, which does not have "IDE" in its name, but is meant to approximate things you see routinely in Netbeans or IntelliJ IDEA --- for proof texts instead of Java code.