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