The theorem prover HOL Light is a close cousin of Isabelle/HOL and doesn't adopt this, and just says that x/0 is some unspecified number. You can't prove much interesting about it. You can prove, say, that x/0 * 0 = 0, but you can't prove whether or not x/0 is, say, positive or not.

If you prefer null, there was a logic that allowed for undefined terms and partial functions that became the basis of the IMPS theorem prover. I found it most notable for the fact that it doesn't have reflexivity of equality: 1/0 = 1/0 is false in IMPS.