PageSourceSearch

https://hol-theorem-prover.org/

html hol-theorem-prover.org collected 2026-09-24 19:24:03 UTC 2,270 bytes, 34 lines download raw bytes

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> &middot; <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>&nbsp;&nbsp;&nbsp;
28<a href="http://jigsaw.w3.org/css-validator/validator?uri=https://hol-theorem-prover.org/style.css" class="footnotelink">Valid CSS</a>&nbsp;&nbsp;&nbsp;
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.