src/HOL/Nominal/INSTALL
author haftmann
Wed Jun 17 08:13:05 2009 +0200 (2009-06-17 ago)
changeset 31671 81e5e8ffe92f
parent 28504 7ad7d7d6df47
permissions -rw-r--r--
datatype packages: record datatype_config for configuration flags; less verbose signatures
urbanc@19754
     1
urbanc@19754
     2
Installation Notes for the Nominal Datatype Package
urbanc@19754
     3
===================================================
urbanc@19754
     4
urbanc@20605
     5
Although the nominal datatype package is an official
urbanc@20605
     6
package in the development snapshot of Isabelle, we 
urbanc@20605
     7
keep a semi-official snapshot of Isabelle and Nominal 
urbanc@20605
     8
under
urbanc@19983
     9
urbanc@19983
    10
  http://isabelle.in.tum.de/nominal/
urbanc@19754
    11
urbanc@19983
    12
This snapshot contains the latest stable release of the
urbanc@19983
    13
nominal datatype package.
urbanc@19754
    14
webertj@20127
    15
To install it, follow the instructions of Isabelle's INSTALL
webertj@20127
    16
about how a snap-shot can be set up. The building process
webertj@20127
    17
needs to be started inside the [ISABELLE_HOME] directory with
urbanc@19983
    18
the command:
urbanc@19754
    19
urbanc@19754
    20
   ./build -m HOL-Nominal
urbanc@19754
    21
urbanc@19754
    22
After the build completes, install the files with the command
urbanc@19754
    23
wenzelm@28504
    24
   ./bin/isabelle install -p /usr/local/bin
urbanc@19754
    25
urbanc@20605
    26
where /usr/local/bin needs to be replaced by an appropriate
urbanc@20605
    27
directory, if you are not root on the system. 
urbanc@20605
    28
webertj@20127
    29
The sources of the nominal datatype package can be found
urbanc@19983
    30
in the directory
urbanc@19754
    31
urbanc@19754
    32
    [ISABELLE_HOME]/src/HOL/Nominal
urbanc@19754
    33
urbanc@19754
    34
The examples are in
urbanc@19754
    35
urbanc@19754
    36
    [ISABELLE_HOME]/src/HOL/Nominal/Examples
urbanc@19754
    37
urbanc@19754
    38
Starting Isabelle with the Nominal Datatype Package Preloaded
urbanc@19754
    39
=============================================================
urbanc@19754
    40
urbanc@20605
    41
Isabelle and the Proof-General interface can be started
urbanc@20605
    42
with
urbanc@19754
    43
urbanc@19754
    44
  Isabelle -L HOL-Nominal <<theory file to be opened>> &
urbanc@19754
    45
urbanc@20605
    46
on the command-line. This automatically loads the correct 
urbanc@20605
    47
keyword file needed for the nominal datatype package.
urbanc@20605
    48
urbanc@20605
    49
Problems with starting Isabelle and Proof-General usually 
urbanc@20605
    50
come from old versions of Proof-General. So make sure you 
urbanc@20605
    51
have installed at least the version ProofGeneral-3.6pre050930.
urbanc@20605
    52
urbanc@20605
    53
If you have problems or comments about the installation process,
urbanc@20605
    54
please make use of the nominal mailing list at
urbanc@20605
    55
urbanc@20605
    56
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/nominal-isabelle/
urbanc@20605
    57