Thanks Chun and Ramana. On 11/09/17 06:26, Chun Tian (binghe) wrote: > Well .. I didn’t reply to the mailing list because it contains some insulting > words to third-party products. But since you forwarded it already, I’m fine > with that.
Oops. I am sorry for that. > I didn’t know you were looking for formalizations of pure mathematics > theories, but here is my another little experience: […] I see. Good idea. > The only sad thing is, this web site didn’t mention any work done in HOL4 > (and its predecessors). While the closest one is HOL light, of course. I > think migrating theories to HOL4 from other theorem provers is not always > straightforward but still doesn’t create much academic value, unless you can > push the related theories to a higher level. I agree. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
