Proofs in mathematicsconsist of a sequence of steps which show statements are true, using ordinarymathematical notation, with the final statement being the theorem proven. Why doesn't HOL translate it's proofs intothis format so that ordinary mathematicians can read it? This is the format and notation used bymathematicians for hundreds of years.
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
