equal
deleted
inserted
replaced
19 <dl> |
19 <dl> |
20 |
20 |
21 <dt><a |
21 <dt><a |
22 href="library/HOL/index.html"><strong>Isabelle/HOL</strong></a><dd> is |
22 href="library/HOL/index.html"><strong>Isabelle/HOL</strong></a><dd> is |
23 a version of classical higher-order logic resembling that of the <A |
23 a version of classical higher-order logic resembling that of the <A |
24 HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL |
24 HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</A>. The |
25 System</A>. |
25 main libraries of the HOL 4 System are now <a |
|
26 href="library/HOL/HOL-Complex/HOL4/index.html">available in |
|
27 Isabelle</a>. |
26 |
28 |
27 <dt><a |
29 <dt><a |
28 href="library/HOLCF/index.html"><strong>Isabelle/HOLCF</strong></a><dd> |
30 href="library/HOLCF/index.html"><strong>Isabelle/HOLCF</strong></a><dd> |
29 adds Scott's Logic for Computable Functions (domain theory) to HOL. |
31 adds Scott's Logic for Computable Functions (domain theory) to HOL. |
30 |
32 |