src/ZF/IMP/README.html
changeset 51403 2ff3a5589b05
parent 51402 b05cd411d3d3
child 51404 90a598019aeb
--- a/src/ZF/IMP/README.html	Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-<!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>ZF/IMP/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2>
-
-The formalization of the denotational and operational semantics of a simple
-while-language together with an equivalence proof between the two semantics.
-The whole development essentially formalizes/transcribes chapters 2 and 5 of
-<P>
-<PRE>
-@book{Winskel,
- author = {Glynn Winskel},
- title = {The Formal Semantics of Programming Languages},
- publisher = {MIT Press},
- year = 1993}.
-</PRE>
-<P>
-There is a
-<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz">report</A>
-by L&ouml;tzbeyer and Sandner.
-<P>
-A much extended version of this development is found in
-<A HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
-</BODY></HTML>