|
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 |
|
|
|
24 |
./bin/isatool install -p /usr/local/bin
|
|
|
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 |
|