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