Re: [isabelle] Inequality assumption
On 05.07.2016 17:27, Lawrence Paulson wrote:
We have taken the liberty of extending division with x/0 = 0 precisely so that a great many theorems, including the one you mention, can be proved more generally.
Hmm, than it would still more useful to replace False by Truth, which
makes Truth and Truth a much more refreshing experience and a happier
Well, the nasty thing here IMHO is: dividing by zero might be permitted,
but can't be zero, it's negativ or positiv infinity, resp. |infinity| -
quite different from 0.
not that much surprised.
This archive was generated by a fusion of
Pipermail (Mailman edition) and