added a fresh_left lemma that contains all instantiation
for the various atom-types.
<?xml version='1.0' encoding='iso-8859-1' ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<!-- $Id$ -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Community</title>
<?include file="//include/htmlheader.include.html"?>
</head>
<body class="main">
<?include file="//include/header.include.html"?>
<div class="hr"><hr/></div>
<?include file="//include/navigation.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
<h2>Project partners</h2>
<p>Isabelle is a joint project between
<a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>
(<a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">University of Cambridge</a>, UK) and
<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>
(<a href="http://www4.in.tum.de/proj/theoremprov/group.html">Technical University of Munich</a>, Germany).</p>
<p>There is an (incomplete) list of past and present <a href=
"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html">projects</a>
undertaken using Isabelle.</p>
<h2>Mailing list</h2>
<p>You may use the mailing list <a href=
"mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> and its
<a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to discuss
problems and results. To subscribe, <a href=
"mailto:Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe">
contact our robot</a>.</p>
<h2>Contributing theorems</h2>
<p>Did you have to prove a lemma that should have been part
of the Isabelle distribution? Send it to us!</p>
<p>We will collect theorems sent to <a href=
"mailto:isabelle-lemmas@cl.cam.ac.uk">isabelle-lemmas@cl.cam.ac.uk</a>.
Accepted material will be included in the Isabelle sources, with credit given
to the author. Note that the Isabelle sources are distributed under the BSD
license. Lemmas should be general, useful, and not too large. For larger
developments you might want to consider a submission to the
<a href="http://afp.sf.net">Archive of Formal Proofs</a>.</p>
<h2 id="afp">The Archive of Formal Proofs (AFP)</h2>
<p>The <a href="http://afp.sf.net">Archive of Formal Proofs</a> is a collection of proof
libraries, examples, and larger scientifc developments, mechanically checked
in Isabelle. It is organized in the way of a scientific journal. Submissions
are refereed.</p>
</div>
<div class="hr"><hr/></div>
<?include file="//include/footer.include.html"?>
</body>
</html>