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