# Re: [isabelle] Where to learn about HOL vs FOL?

• To: cl-isabelle-users at lists.cam.ac.uk
• Subject: Re: [isabelle] Where to learn about HOL vs FOL?
• From: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>
• Date: Wed, 01 Jan 2014 20:28:11 +0100
• References: <op.wrrj47uzule2fv@cardamome> <510A79F0.9050308@gmx.com> <CAAPnxw2g6Di9MEmQgyqhf_+NBW5HLrVAPi2JVxohcFLTqWe1dA@mail.gmail.com> <op.wrsjuyeuule2fv@cardamome> <510BCFBD.1020103@gmx.com>
• User-agent: Opera Mail/12.16 (Linux)

Le Fri, 01 Feb 2013 15:22:53 +0100, Gottfried Barrow <gottfried.barrow at gmx.com> a écrit:
```
```
```[…]

```
For HOL4 they already have that in their logic manual (to what degree I can't say), which I thought would be the perfect place to learn about Isabelle/HOL's formal logic, but it's not, it's the perfect place to learn about HOL4's formal logic:
```
http://hol.sourceforge.net/documentation.html
[…]
```
```
```
The one titled “Logic” (file name “kananaskis-8-logic.pdf”) still says in the preface:
```
```
```This material was written by Andrew Pitts in 1991, and was
originally part of DESCRIPTION. Because this logic is shared
with other theorem-proving systems (HOL Light, ProofPower),
and is similar to that implemented in Isabelle, where it is
called Isabelle/HOL, it is now presented in its own manual.
```
```

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.