[Hol-info] Rigour Vs expressiveness

[Francis.Flannery <Fra...@ul...>]

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