1 |
|
2 Installation Notes for the Nominal Datatype Package |
|
3 =================================================== |
|
4 |
|
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 |
|
9 |
|
10 http://isabelle.in.tum.de/nominal/ |
|
11 |
|
12 This snapshot contains the latest stable release of the |
|
13 nominal datatype package. |
|
14 |
|
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 |
|
18 the command: |
|
19 |
|
20 ./build -m HOL-Nominal |
|
21 |
|
22 After the build completes, install the files with the command |
|
23 |
|
24 ./bin/isabelle install -p /usr/local/bin |
|
25 |
|
26 where /usr/local/bin needs to be replaced by an appropriate |
|
27 directory, if you are not root on the system. |
|
28 |
|
29 The sources of the nominal datatype package can be found |
|
30 in the directory |
|
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 |
|
41 Isabelle and the Proof-General interface can be started |
|
42 with |
|
43 |
|
44 Isabelle -L HOL-Nominal <<theory file to be opened>> & |
|
45 |
|
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 |
|