|
19754
|
1 |
|
|
|
2 |
Installation Notes for the Nominal Datatype Package
|
|
|
3 |
===================================================
|
|
|
4 |
|
|
19983
|
5 |
Although the nominal datatype package is now officially
|
|
|
6 |
part of the development snapshot of Isabelle, we keep
|
|
|
7 |
a semi-official nominal snapshot under
|
|
|
8 |
|
|
|
9 |
http://isabelle.in.tum.de/nominal/
|
|
19754
|
10 |
|
|
19983
|
11 |
This snapshot contains the latest stable release of the
|
|
|
12 |
nominal datatype package.
|
|
19754
|
13 |
|
|
19983
|
14 |
To install it, follow the instructions of Isabelle's INSTALL
|
|
|
15 |
about how a snap-shot can be set up. The building process
|
|
|
16 |
needs to be started inside the [ISABELLE_HOME] directory with
|
|
|
17 |
the command:
|
|
19754
|
18 |
|
|
|
19 |
./build -m HOL-Nominal
|
|
|
20 |
|
|
|
21 |
After the build completes, install the files with the command
|
|
|
22 |
|
|
|
23 |
./bin/isatool install -p /usr/local/bin
|
|
|
24 |
|
|
19983
|
25 |
The sources of the nominal datatype package can be found
|
|
|
26 |
in the directory
|
|
19754
|
27 |
|
|
|
28 |
[ISABELLE_HOME]/src/HOL/Nominal
|
|
|
29 |
|
|
|
30 |
The examples are in
|
|
|
31 |
|
|
|
32 |
[ISABELLE_HOME]/src/HOL/Nominal/Examples
|
|
|
33 |
|
|
|
34 |
Starting Isabelle with the Nominal Datatype Package Preloaded
|
|
|
35 |
=============================================================
|
|
|
36 |
|
|
|
37 |
Isabelle including the Proof-General interface can be started
|
|
|
38 |
|
|
|
39 |
Isabelle -L HOL-Nominal <<theory file to be opened>> &
|
|
|
40 |
|
|
|
41 |
This automatically loads the correct keyword file needed
|
|
|
42 |
for the nominal datatype package.
|