README
author wenzelm
Wed, 14 Feb 2024 14:41:18 +0100
changeset 79604 0e8ac7db1f4d
parent 73530 89cf7c903aca
permissions -rw-r--r--
clarified num_processors: follow Poly/ML (with its inaccuracies);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
     1
The Isabelle System Distribution
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
     2
================================
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
     3
73530
89cf7c903aca clarified README;
wenzelm
parents: 71337
diff changeset
     4
See the NEWS file in the distribution for details on user-relevant
89cf7c903aca clarified README;
wenzelm
parents: 71337
diff changeset
     5
changes.  The ANNOUNCE file recounts notable changes for the latest
89cf7c903aca clarified README;
wenzelm
parents: 71337
diff changeset
     6
official release.
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
     7
73530
89cf7c903aca clarified README;
wenzelm
parents: 71337
diff changeset
     8
The core of Isabelle is subject to a 3-clause BSD license, but add-on
89cf7c903aca clarified README;
wenzelm
parents: 71337
diff changeset
     9
components have their own license schemes (similar to a Linux
89cf7c903aca clarified README;
wenzelm
parents: 71337
diff changeset
    10
distribution).
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    11
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    12
47795
ccb10fe4b955 some updates on classic README, reduce the impression that there is much to install manually;
wenzelm
parents: 47745
diff changeset
    13
Installation
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    14
------------
33842
efa1b89c79e0 misc tuning and updates for official release;
wenzelm
parents: 32361
diff changeset
    15
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    16
Isabelle works on the three main platform families: Linux, Windows,
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    17
and macOS.  The application bundles from the Isabelle web page
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    18
include sources, documentation, and add-on tools for all supported
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    19
platforms.
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    20
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    21
Some technical background information may be found in the Isabelle
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    22
System Manual (directory doc).
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    23
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    24
57452
ecad2a53755a misc updates for release;
wenzelm
parents: 54051
diff changeset
    25
User interface
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    26
--------------
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    27
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    28
Isabelle/jEdit is an advanced Prover IDE based on jEdit and
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    29
Isabelle/Scala.  It is the main example application of the
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    30
Isabelle/PIDE framework, and the default user interface of
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    31
Isabelle.  It provides a metaphor of continuous proof checking of a
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    32
versioned collection of theory sources, with instantaneous feedback
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    33
in real-time and rich semantic markup associated with the formal
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    34
text.
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    35
41596
e424bc65080d misc updates for release;
wenzelm
parents: 41527
diff changeset
    36
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    37
Other sources of information
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    38
----------------------------
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    39
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    40
  * The Isabelle Page
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    41
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    42
    The Isabelle home page may be accessed from the following mirror
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    43
    sites:
50572
b33912e68b84 updated README;
wenzelm
parents: 47805
diff changeset
    44
68649
f849fc1cb65e prefer HTTPS;
wenzelm
parents: 67866
diff changeset
    45
     * https://www.cl.cam.ac.uk/research/hvg/Isabelle
f849fc1cb65e prefer HTTPS;
wenzelm
parents: 67866
diff changeset
    46
     * https://isabelle.in.tum.de
70025
16042475c511 misc tuning for release;
wenzelm
parents: 68649
diff changeset
    47
     * https://mirror.cse.unsw.edu.au/pub/isabelle
68649
f849fc1cb65e prefer HTTPS;
wenzelm
parents: 67866
diff changeset
    48
     * https://mirror.clarkson.edu/isabelle
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    49
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    50
  * Mailing list
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    51
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    52
    The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    53
    forum for Isabelle users to discuss problems and exchange
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    54
    information.  To join, send a message to
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    55
    isabelle-users-request@cl.cam.ac.uk.
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    56
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    57
  * Personal mail
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    58
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    59
    Lawrence C Paulson
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    60
    Computer Laboratory
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    61
    University of Cambridge
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    62
    JJ Thomson Avenue
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    63
    Cambridge CB3 0FD
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    64
    England
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    65
    E-mail: lcp@cl.cam.ac.uk
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    66
    Phone: +44-223-763500
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    67
    Fax: +44-223-334748
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    68
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    69
    or
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    70
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    71
    Tobias Nipkow
71337
wenzelm
parents: 71336
diff changeset
    72
    Institut für Informatik
wenzelm
parents: 71336
diff changeset
    73
    Technische Universität München
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    74
    Boltzmannstr. 3
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    75
    D-85748 Garching
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    76
    Germany
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    77
    E-mail: nipkow@in.tum.de
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    78
    Phone: +49-89-289-17302
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    79
    Fax: +49-89-289-17307
25214
91730b492a45 ASCIIfied README
haftmann
parents:
diff changeset
    80
71336
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    81
NOTE:
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    82
    Please report any problems you encounter. While we shall try to be
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    83
    helpful, we can accept no responsibility for the deficiencies of
b9a9afa70d1a improved Markdown-like display in Phabricator;
wenzelm
parents: 70025
diff changeset
    84
    Isabelle and their consequences.