1% Release notes for HOL4, ??????
2
3<!-- search and replace ?????? strings corresponding to release name -->
4<!-- indent code within bulleted lists to column 11 -->
5
6(Released: ???)
7
8We are pleased to announce the ?????? release of HOL 4.
9
10Contents
11--------
12
13-   [New features](#new-features)
14-   [Bugs fixed](#bugs-fixed)
15-   [New theories](#new-theories)
16-   [New tools](#new-tools)
17-   [New Examples](#new-examples)
18-   [Incompatibilities](#incompatibilities)
19
20New features:
21-------------
22
23Bugs fixed:
24-----------
25
26New theories:
27-------------
28
29*   `real_topologyTheory`: a rather complete theory of Elementary
30    Topology in Euclidean Space, ported by Muhammad Qasim and Osman
31    Hasan from HOL-light (up to 2015). The part of General Topology
32    (independent of `realTheory`) is now available at
33    `topologyTheory`; the old `topologyTheory` is renamed to
34    `metricTheory`.
35
36    There is a minor backwards-incompatibility: old proof scripts using
37    the metric-related results in previous `topologyTheory` should now
38    open `metricTheory` instead. (Thanks to Chun Tian for this work.)
39
40New tools:
41----------
42
43New examples:
44---------
45
46Incompatibilities:
47------------------
48
49*   The `Holmake` tool now behaves with the `--qof` behaviour enabled by default.
50    This means that script files which have a tactic failure occur will cause the building of the corresponding theory to fail, rather than having the build continue with the theorem ���cheated���.
51    We think this will be less confusing for new users.
52    Experts who *do* want to have script files continue past such errors can use the `--noqof` option to enable the old behaviour.
53
54*   When running with Poly/ML, we now require at least version 5.7.0.
55
56* * * * *
57
58<div class="footer">
59*[HOL4, ??????](http://hol-theorem-prover.org)*
60
61[Release notes for the previous version](kananaskis-12.release.html)
62
63</div>
64