|
From: Francis.Flannery <Fra...@ul...> - 2004-04-08 14:26:31
|
Hi, The HOL system seems a allow a more flexible method of automating proof. Therefore its rigour is lessened to achieve this. For example its rules are not represented as explicit structures as in the HOL system. Also I believe Isabelle is based on a more rigourous type of set theory than the HOL system. Is this a true generalisation? And could someone tell me if their is any relevant documentation that compares these two systems? Please let me know if this is untrue. Francis Flannery |