equal
deleted
inserted
replaced
25 <p>The Isabelle distribution includes a large body of |
25 <p>The Isabelle distribution includes a large body of |
26 object logics and other examples (see the <a href= |
26 object logics and other examples (see the <a href= |
27 "//dist/library/index.html">Isabelle theory library</a>).</p> |
27 "//dist/library/index.html">Isabelle theory library</a>).</p> |
28 |
28 |
29 <dl> |
29 <dl> |
30 <dt id="isabelle_hol"><a href="//dist/library/HOL/index.html">Isabelle/HOL</a></dt> |
30 <dt id="isabelle_hol"><a |
31 <dd>is a version of classical higher-order logic resembling that of the |
31 href="//dist/library/HOL/index.html">Isabelle/HOL</a></dt> |
32 <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>. The |
32 <dd>is a version of classical higher-order logic resembling |
33 main libraries of the HOL 4 System are now <a href= |
33 that of the <a |
34 "//dist/library/HOL/HOL-Complex/HOL4/index.html">available in Isabelle</a>.</dd> |
34 href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL |
|
35 System</a>.</dd> |
35 |
36 |
36 <dt><a href= |
37 <dt><a href= |
37 "//dist/library/HOLCF/index.html">Isabelle/HOLCF</a></dt> |
38 "//dist/library/HOLCF/index.html">Isabelle/HOLCF</a></dt> |
38 <dd>adds Scott's Logic for Computable Functions (domain theory) to |
39 <dd>adds Scott's Logic for Computable Functions (domain theory) to |
39 HOL.</dd> |
40 HOL.</dd> |