Reintroduce set_interpreter for Collect and op :.
I removed them by accident when removing old code that dealt with the "set" type.
Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
<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ö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>