> Osmosis. The original HOL documentation/code included schematic
derivations of the derived rules of inference (didn't that
> make it into Gordon and Melham?). However, the starting point for that is
the rather ad hoc collection of primitive rules and
> axioms that evolved into the ones currently
Our apologies if you have received multiple copies.
THIRD CALL FOR PAPERS
FMICS 2014
19th International Workshop on
Formal Methods for Industrial Critical Systems
11-12 September 2014, Florence, Italy
In co-location wi
Bill,
On 24 Mar 2014, at 06:28, Bill Richter wrote:
> Thanks, Rob! You're right, I hadn't looked at Section 1.4 "A Formulation
> Based on Equality" of Andrew's link
>> http://plato.stanford.edu/entries/type-theory-church/ and more to the point,
>> I didn't read the longer version Andrew's wro
Mark, I tried to make your corrections, and here's my new draft, at just 500
lines:
I want to explain how to read the HOL Light basics from the source code in
several sections
0) informal math and HOL
1) the type bool and the constant =
2) sequents, new_basic_definition and the HOL Light infere
