Admin/page/main-content/index.content
author kleing
Fri, 29 Apr 2005 13:11:19 +0200
changeset 15885 7274ba411f1d
parent 15777 311aedc96e71
permissions -rw-r--r--
include new thms_containing
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     1
%title%
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     2
Isabelle
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     3
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     4
%body%
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     5
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     6
<p>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     7
10050
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
     8
<h2>What is Isabelle?</h2>
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
     9
10019
wenzelm
parents: 10016
diff changeset
    10
Isabelle is a popular generic theorem proving environment developed at
wenzelm
parents: 10016
diff changeset
    11
Cambridge University (<a
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    12
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    13
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
14230
def0606302a1 Added overview page.
berghofe
parents: 13848
diff changeset
    14
See the <a href="overview.html">Isabelle overview</a>.
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    15
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    16
<p>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    17
9285
21bfc8c14c3d about -> logics, better access to online libraries
kleing
parents: 8221
diff changeset
    18
These pages provide general information on Isabelle, more specific
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    19
information is available from the local pages
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    20
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    21
<ul>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    22
11109
wenzelm
parents: 10162
diff changeset
    23
<li><a
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    24
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
11109
wenzelm
parents: 10162
diff changeset
    25
at Cambridge</strong></a>
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    26
13087
879ac452101e inserted tutorial
kleing
parents: 11109
diff changeset
    27
<li><a href="http://www4.in.tum.de/proj/theoremprov/group.html"><strong>Isabelle
11109
wenzelm
parents: 10162
diff changeset
    28
at Munich</strong></a>
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    29
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    30
</ul>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    31
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    32
See there for information on projects done with Isabelle, mailing list
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    33
archives, research papers, the Isabelle bibliography, and Isabelle
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    34
workshops and courses.
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    35
10050
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
    36
<p>
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    37
15420
45653714db88 Isabelle 2005 - preview
kleing
parents: 15282
diff changeset
    38
<h2>Isabelle 2005 - Preview</h2>
45653714db88 Isabelle 2005 - preview
kleing
parents: 15282
diff changeset
    39
45653714db88 Isabelle 2005 - preview
kleing
parents: 15282
diff changeset
    40
<ul>
15777
311aedc96e71 added locale instantiation
kleing
parents: 15559
diff changeset
    41
<li>New commands for instantiating locales</li>
15420
45653714db88 Isabelle 2005 - preview
kleing
parents: 15282
diff changeset
    42
<li>New command for finding matching rewrite rules</li>
15885
7274ba411f1d include new thms_containing
kleing
parents: 15777
diff changeset
    43
<li>Finding theorems by term patterns</li>
15420
45653714db88 Isabelle 2005 - preview
kleing
parents: 15282
diff changeset
    44
<li>New automatic transitivity reasoner</li>
45653714db88 Isabelle 2005 - preview
kleing
parents: 15282
diff changeset
    45
<li>New command for ad-hoc theory viewing and printing</li>
15515
9bc5aff80976 more preview
kleing
parents: 15514
diff changeset
    46
<li>Much extended and improved theory of finite sets</li>
15777
311aedc96e71 added locale instantiation
kleing
parents: 15559
diff changeset
    47
<li>New syntax that will allow &gt; and &gt;= in addition to &lt; and &lt;=</li>
15420
45653714db88 Isabelle 2005 - preview
kleing
parents: 15282
diff changeset
    48
</ul>
45653714db88 Isabelle 2005 - preview
kleing
parents: 15282
diff changeset
    49
15514
a8b4c9a87e85 pointer to isabelle-lemmas submission list
kleing
parents: 15420
diff changeset
    50
<h2>Contributing</h2> 
a8b4c9a87e85 pointer to isabelle-lemmas submission list
kleing
parents: 15420
diff changeset
    51
a8b4c9a87e85 pointer to isabelle-lemmas submission list
kleing
parents: 15420
diff changeset
    52
Did you have to prove a lemma that should have been part of the
15553
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
    53
Isabelle distribution?  Send it to us!  <p> We will collect theorems
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
    54
sent to <a
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
    55
href="&#109;&#97;&#105;&#108;&#116;&#111;:&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#108;&#101;&#109;&#109;&#97;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;">&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#108;&#101;&#109;&#109;&#97;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;</a>.
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
    56
Accepted material will be included in the Isabelle sources, with
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
    57
credit given to the author. Note that the Isabelle sources are
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
    58
distributed under the BSD license.  Lemmas should be general, useful,
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
    59
and not too large. For larger developments you might want to consider
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
    60
a submission to the <a href="http://afp.sf.net">Archive of Formal
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
    61
Proofs</a>.
15514
a8b4c9a87e85 pointer to isabelle-lemmas submission list
kleing
parents: 15420
diff changeset
    62
a8b4c9a87e85 pointer to isabelle-lemmas submission list
kleing
parents: 15420
diff changeset
    63
15282
765d5d6e4468 Exercises added
webertj
parents: 15276
diff changeset
    64
<h2>Course Material, Exercises</h2>
15137
8a17799687e7 include course material page
kleing
parents: 14667
diff changeset
    65
8a17799687e7 include course material page
kleing
parents: 14667
diff changeset
    66
The <a
8a17799687e7 include course material page
kleing
parents: 14667
diff changeset
    67
href="http://isabelle.in.tum.de/coursematerial/">course material</a>
8a17799687e7 include course material page
kleing
parents: 14667
diff changeset
    68
page makes slides, demos, and exercises of a growing number of
15138
9390018ea712 improved wording course material
kleing
parents: 15137
diff changeset
    69
Isabelle courses available. It is meant as a resource for people 
9390018ea712 improved wording course material
kleing
parents: 15137
diff changeset
    70
who would like to learn Isabelle as well as for those who would like 
9390018ea712 improved wording course material
kleing
parents: 15137
diff changeset
    71
to teach it.
15137
8a17799687e7 include course material page
kleing
parents: 14667
diff changeset
    72
8a17799687e7 include course material page
kleing
parents: 14667
diff changeset
    73
<p>
8a17799687e7 include course material page
kleing
parents: 14667
diff changeset
    74
14667
5a899cd54366 added AFP
kleing
parents: 14637
diff changeset
    75
<h2>AFP - The Archive of Formal Proofs</h2>
5a899cd54366 added AFP
kleing
parents: 14637
diff changeset
    76
5a899cd54366 added AFP
kleing
parents: 14637
diff changeset
    77
The <a href="http://afp.sf.net">Archive of Formal Proofs</a> is a
5a899cd54366 added AFP
kleing
parents: 14637
diff changeset
    78
collection of proof libraries, examples, and larger scientifc
5a899cd54366 added AFP
kleing
parents: 14637
diff changeset
    79
developments, mechanically checked in Isabelle. It is organized in the
5a899cd54366 added AFP
kleing
parents: 14637
diff changeset
    80
way of a scientific journal. Submissions are refereed.
5a899cd54366 added AFP
kleing
parents: 14637
diff changeset
    81
5a899cd54366 added AFP
kleing
parents: 14637
diff changeset
    82
<p>
5a899cd54366 added AFP
kleing
parents: 14637
diff changeset
    83
14576
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    84
<h2><!-- _GP_ distname --></h2>
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    85
New features in <strong><!-- _GP_ distname --></strong> include
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    86
<ul>
14624
9b3397a848c3 add HOL4
kleing
parents: 14615
diff changeset
    87
<li>New image HOL4 with imported library from HOL4 system on top of
9b3397a848c3 add HOL4
kleing
parents: 14615
diff changeset
    88
  HOL-Complex (about 2500 additional theorems).</li>
9b3397a848c3 add HOL4
kleing
parents: 14615
diff changeset
    89
14576
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    90
<li>New theory Ring_and_Field with over 250 basic numerical laws, 
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    91
  all proved in axiomatic type classes for semirings, rings and fields.</li>
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    92
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    93
<li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li>
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    94
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    95
<li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    96
14611
e9d2f771b3c7 add HOL-Matrix
kleing
parents: 14582
diff changeset
    97
<li>New theory of matrices with an application to linear programming in HOL-Matrix.</li>
e9d2f771b3c7 add HOL-Matrix
kleing
parents: 14582
diff changeset
    98
14576
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
    99
<li>Improved locales (named proof contexts), instantiation of locales.</li>
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   100
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   101
<li>Improved handling of linear and partial orders in simplifier.</li>
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   102
 
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   103
<li>New <code>specification</code> command for definition by specification.</li>  
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   104
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   105
<li>New Isar command <code>finalconsts</code> prevents constants being given a definition later.</li>  
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   106
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   107
<li><code>arith</code> now generates counterexamples for reals as well.</li>
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   108
14580
b9fd5e39b695 *** empty log message ***
nipkow
parents: 14576
diff changeset
   109
<li>New <code>quickcheck</code> command
14615
603f08285c65 small additions
nipkow
parents: 14611
diff changeset
   110
    to search for counterexamples of executable goals.
603f08285c65 small additions
nipkow
parents: 14611
diff changeset
   111
  (see HOL/ex/Quickcheck_Examples.thy)</li>
14580
b9fd5e39b695 *** empty log message ***
nipkow
parents: 14576
diff changeset
   112
<li>New <code>refute</code> command
14615
603f08285c65 small additions
nipkow
parents: 14611
diff changeset
   113
    to search for finite countermodels of goals.
603f08285c65 small additions
nipkow
parents: 14611
diff changeset
   114
  (see HOL/ex/Refute_Examples.thy)
603f08285c65 small additions
nipkow
parents: 14611
diff changeset
   115
</li>
14576
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   116
14615
603f08285c65 small additions
nipkow
parents: 14611
diff changeset
   117
<li>Presentation and x-symbol enhancements, greek letters and
603f08285c65 small additions
nipkow
parents: 14611
diff changeset
   118
sub/superscripts allowed in identifiers.</li>
14576
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   119
</ul>
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   120
<a href="dist/<!-- _GP_ distname -->/NEWS">[Complete Changelog]</a>
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   121
<p>
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   122
The <strong><!-- _GP_ distname --></strong> distribution is available
37a92211a5d3 add feature list
kleing
parents: 14379
diff changeset
   123
from several <a href="dist/index.html">mirror sites</a>.  It includes
14637
d258f6c11d83 removed 'tutorial out now' (out of date)
kleing
parents: 14624
diff changeset
   124
source and binary packages and browsable documentation. You can also
d258f6c11d83 removed 'tutorial out now' (out of date)
kleing
parents: 14624
diff changeset
   125
browse the <a href="library/index.html">Isabelle theory library</a>
d258f6c11d83 removed 'tutorial out now' (out of date)
kleing
parents: 14624
diff changeset
   126
online. For the curious, there is a nightly generated <a
d258f6c11d83 removed 'tutorial out now' (out of date)
kleing
parents: 14624
diff changeset
   127
href="http://isabelle.in.tum.de/devel/">development snapshot</a>
d258f6c11d83 removed 'tutorial out now' (out of date)
kleing
parents: 14624
diff changeset
   128
available.
8070
dbbef2367723 some tuning (incorporated David's suggestions)
kleing
parents: 8060
diff changeset
   129
10050
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
   130
<p>
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   131
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   132
<h2>Mailing list</h2>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   133
15553
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
   134
Use the mailing list <a
2b3f9c493259 spider dogding
kleing
parents: 15527
diff changeset
   135
href="&#109;&#97;&#105;&#108;&#116;&#111;:&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#117;&#115;&#101;&#114;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;">&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#117;&#115;&#101;&#114;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;</a>
14379
ea10a8c3e9cf updated links to the old ftp site
paulson
parents: 14230
diff changeset
   136
and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to
15559
10c5c689aa20 obscured the e-mail address lcp@cl
paulson
parents: 15553
diff changeset
   137
discuss problems and results.  To subscribe, <a href="&#109;&#97;&#105;&#108;&#116;&#111;:&#108;&#99;&#112;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">contact Larry Paulson</a>.
10050
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
   138