--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/README.html	Sat Nov 27 16:08:10 2010 -0800
@@ -0,0 +1,45 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
+<html>
+
+<head>
+  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+  <title>HOLCF/README</title>
+</head>
+
+<body>
+
+<h3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</h3>
+
+HOLCF is the definitional extension of Church's Higher-Order Logic with
+Scott's Logic for Computable Functions that has been implemented in the
+theorem prover Isabelle.  This results in a flexible setup for reasoning
+about functional programs. HOLCF supports standard domain theory (in particular
+fixpoint reasoning and recursive domain equations) but also coinductive
+arguments about lazy datatypes.
+
+<p>
+
+The most recent description of HOLCF is found here:
+
+<ul>
+  <li><a href="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</a>
+</ul>
+
+A detailed description (in German) of the entire development can be found in:
+
+<ul>
+  <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf">HOLCF: eine konservative Erweiterung von HOL um LCF</a>, <br>
+      Franz Regensburger.<br>
+      Dissertation Technische Universit&auml;t M&uuml;nchen.<br>
+      Year: 1994.
+</ul>
+
+A short survey is available in:
+<ul>
+  <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</a><br>
+</ul>
+
+</body>
+
+</html>
changeset 40774	0437dbc127b3
parent 35174	e15040ae75d7
child 47839	3c54878ed67b