author | nipkow |
Sat, 20 Jun 2009 01:53:39 +0200 | |
changeset 31729 | b9299916d618 |
parent 28504 | 7ad7d7d6df47 |
permissions | -rw-r--r-- |
19754 | 1 |
|
2 |
Installation Notes for the Nominal Datatype Package |
|
3 |
=================================================== |
|
4 |
||
20605 | 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 |
|
19983 | 9 |
|
10 |
http://isabelle.in.tum.de/nominal/ |
|
19754 | 11 |
|
19983 | 12 |
This snapshot contains the latest stable release of the |
13 |
nominal datatype package. |
|
19754 | 14 |
|
20127 | 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 |
|
19983 | 18 |
the command: |
19754 | 19 |
|
20 |
./build -m HOL-Nominal |
|
21 |
||
22 |
After the build completes, install the files with the command |
|
23 |
||
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
20605
diff
changeset
|
24 |
./bin/isabelle install -p /usr/local/bin |
19754 | 25 |
|
20605 | 26 |
where /usr/local/bin needs to be replaced by an appropriate |
27 |
directory, if you are not root on the system. |
|
28 |
||
20127 | 29 |
The sources of the nominal datatype package can be found |
19983 | 30 |
in the directory |
19754 | 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 |
||
20605 | 41 |
Isabelle and the Proof-General interface can be started |
42 |
with |
|
19754 | 43 |
|
44 |
Isabelle -L HOL-Nominal <<theory file to be opened>> & |
|
45 |
||
20605 | 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 |