1 |
1 |
2 Installation Notes for the Nominal Datatype Package |
2 Installation Notes for the Nominal Datatype Package |
3 =================================================== |
3 =================================================== |
4 |
4 |
5 The nominal datatype package is part of the development |
5 Although the nominal datatype package is now officially |
6 snapshots of Isabelle. Get the sources from |
6 part of the development snapshot of Isabelle, we keep |
|
7 a semi-official nominal snapshot under |
7 |
8 |
8 http://isabelle.in.tum.de/devel/ |
9 http://isabelle.in.tum.de/nominal/ |
9 |
10 |
10 Follow the instructions in INSTALL for how a snap-shot |
11 This snapshot contains the latest stable release of the |
11 can be set up. The building process needs to be started |
12 nominal datatype package. |
12 inside the [ISABELLE_HOME] directory with the command: |
13 |
|
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: |
13 |
18 |
14 ./build -m HOL-Nominal |
19 ./build -m HOL-Nominal |
15 |
20 |
16 After the build completes, install the files with the command |
21 After the build completes, install the files with the command |
17 |
22 |
18 ./bin/isatool install -p /usr/local/bin |
23 ./bin/isatool install -p /usr/local/bin |
19 |
24 |
20 The sources sources of the nominal datatype package |
25 The sources of the nominal datatype package can be found |
21 can be found in the directory |
26 in the directory |
22 |
27 |
23 [ISABELLE_HOME]/src/HOL/Nominal |
28 [ISABELLE_HOME]/src/HOL/Nominal |
24 |
29 |
25 The examples are in |
30 The examples are in |
26 |
31 |