1<!DOCTYPE html> 2<html lang="en"> 3<head> 4 <meta http-equiv="Content-Type" content="text/html; charset=utf-8" > 5 <meta name="viewport" content="width=device-width, initial-scale=1, maximum-scale=1" > 6 <link href='https://fonts.googleapis.com/css?family=Lora' rel='stylesheet' type='text/css'> 7 <link href='https://fonts.googleapis.com/css?family=Bree+Serif' rel='stylesheet' type='text/css'> 8 <link rel="stylesheet" href="style.css"> 9 <title>HOL Interactive Theorem Prover</title> 10</head> 11<body> 12<a class="toprightcorner" href="https://github.com/HOL-Theorem-Prover/HOL"><img src="images/on-github-70.png" id=ongithub alt="on github"></a> 13 14<!-- Title page --> 15 16 <div class="titlepage"> 17 <div class="titlebox_padding"></div> 18 <div class="titlebox_container"><div class="titlebox">HOL<div class="titlebox_subtitle">Interactive Theorem Prover</div></div></div> 19 <div class="newsbox_container"><div class="newsbox"><b><a href="latest.html">Latest</a>:</b> Trindemossen-2 released (see <a href="trindemossen-2.release.html">release notes</a> · <a href="release-notes.html">all release notes</a>).</div></div> 20 <div class="linkbox"><a href="about.html"><div class="blackbox">About</div></a> 21 <a href="install.html"><div class="blackbox">Download and Install</div></a> 22 <a href="/docs/latest/"><div class="blackbox">Documentation</div></a> 23 <a href="community.html"><div class="blackbox">Community</div></a></div> 24 </div> 25 26<div class="footer"> 27<a href="http://validator.w3.org/check?uri=https://hol-theorem-prover.org/index.html" class="footnotelink">Valid HTML</a> 28<a href="http://jigsaw.w3.org/css-validator/validator?uri=https://hol-theorem-prover.org/style.css" class="footnotelink">Valid CSS</a> 29<span class="mobile_version">mobile version</span> 30</div> 31
32<script type="module" src="https://static.cloudflareinsights.com/beacon.min.js/v31edd6df95cf4e85bb4c19e7a9bdbcba1788362987495" integrity="sha512-iIg7k2xntmwu6/uSb5tpc/hySgZc4eoL31yB29W6tJFo2akwjPWcEqnCEdJvGexCL0KEQwVYv5BlowfhVz26hg==" data-cf-beacon='{"version":"2024.11.0","token":"b27051b50a61412d8f35e445ab79c5d8","r":1,"spa":2}' crossorigin="anonymous"></script>
32 33</body> 34</html>
Line numbers count LF bytes from the start of the resource, as the search results do. Vendor segments are library code the classifier recognised; they are stored but not indexed. Bytes are shown as Latin1 characters, one per byte.