None of these attempts make any sense. In HOL and similar systems (including Isabelle/HOL), it’s *impossible* to arrange for x/0 to be undefined in any strong sense. Fortunately, it’s consistent and harmless to put x/0 = 0.
Larry Paulson > On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourceforge.net wrote: > > I run some experiments so to check if it is violating any fundamental rule. > So far it went good. _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
