13 <div class="hr"><hr/></div> |
13 <div class="hr"><hr/></div> |
14 <?include file="//include/navigation.include.html"?> |
14 <?include file="//include/navigation.include.html"?> |
15 <div class="hr"><hr/></div> |
15 <div class="hr"><hr/></div> |
16 <div id="content"> |
16 <div id="content"> |
17 |
17 |
|
18 <h2>Project partners</h2> |
|
19 |
|
20 <p>Isabelle is a joint project between |
|
21 <a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a> |
|
22 (<a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">University of Cambridge</a>, UK) and |
|
23 <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a> |
|
24 (<a href="http://www4.in.tum.de/proj/theoremprov/group.html">Technical University of Munich</a>, Germany).</p> |
|
25 |
|
26 <p>There is an (incomplete) list of past and present <a href= |
|
27 "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html">projects</a> |
|
28 undertaken using Isabelle.</p> |
|
29 |
18 <h2>Mailing list</h2> |
30 <h2>Mailing list</h2> |
19 <p> |
31 |
20 You may use the mailing list <a |
32 <p>You may use the mailing list <a |
21 href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> |
33 href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> |
22 and its <a |
34 and its <a |
23 href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to |
35 href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to |
24 discuss problems and results. To subscribe, <a |
36 discuss problems and results. To subscribe, <a |
25 href="mailto:lcp@cl.cam.ac.uk?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">contact |
37 href="mailto:lcp@cl.cam.ac.uk?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">contact |
37 license. Lemmas should be general, useful, and not too large. For larger |
49 license. Lemmas should be general, useful, and not too large. For larger |
38 developments you might want to consider a submission to the |
50 developments you might want to consider a submission to the |
39 <a href="http://afp.sf.net">Archive of Formal Proofs</a>.</p> |
51 <a href="http://afp.sf.net">Archive of Formal Proofs</a>.</p> |
40 |
52 |
41 <h2 id="afp">The Archive of Formal Proofs (AFP)</h2> |
53 <h2 id="afp">The Archive of Formal Proofs (AFP)</h2> |
|
54 |
42 <p>The <a href="http://afp.sf.net">Archive of Formal Proofs</a> is a collection of proof |
55 <p>The <a href="http://afp.sf.net">Archive of Formal Proofs</a> is a collection of proof |
43 libraries, examples, and larger scientifc developments, mechanically checked |
56 libraries, examples, and larger scientifc developments, mechanically checked |
44 in Isabelle. It is organized in the way of a scientific journal. Submissions |
57 in Isabelle. It is organized in the way of a scientific journal. Submissions |
45 are refereed.</p> |
58 are refereed.</p> |
46 |
59 |