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.

Larry Paulson




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 world ;)

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.

Andreas,
not that much surprised.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.