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, [email protected] wrote: > > I run some experiments so to check if it is violating any fundamental rule. > So far it went good. _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
