Hello Jeremy. Thanks for your reply.
On 05/10/17 13:25, Jeremy Dawson wrote: > Hi Mario, > > I don't mind the question, but the answer may not be much use because > it's a comparison between the 2005 version of Isabelle which I use and > HOL4. > > In terms of the type systems they are identical. > > Isabelle has schematic variables and type classes, both of which can > make proof easier. Otherwise, I don't find major differences. > > Turning to modern day Isabelle - other factors may be: > > - the extent of unnecessarily incompatible changes between one version > of Isabelle and the next (which is in fact why I'm still using the 2005 > version, when I'm not using HOL) > > - the difficulty of using ML to program complex proof tactics - > mandatory for a small proportion of my work (I've had various and highly > conflicting reports of whether this is possible or reasonably easy in > current Isabelle) > > - documentation, and willingness of developers to help with questions > (and for me, location at GMT+10 means I can often get an immediate answer) > > In HOL4 the source code is effectively available for users to look at > (in Isabelle they can look at it, but it - or a lot of it - is highly > obfuscated). > > Cheers, > > Jeremy -- 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
