18 but it is reliable and its database system is convenient for interactive |
18 but it is reliable and its database system is convenient for interactive |
19 work. SML of New Jersey requires lots of store and disc space, but it is |
19 work. SML of New Jersey requires lots of store and disc space, but it is |
20 free and its code sometimes runs faster. Both compilers are perfectly |
20 free and its code sometimes runs faster. Both compilers are perfectly |
21 satisfactory for running Isabelle. |
21 satisfactory for running Isabelle. |
22 |
22 |
23 The Makefiles and make-all use enviroment variables that you should set |
23 The Makefiles and make-all use environment variables that you should set |
24 according to your site configuration. |
24 according to your site configuration. See file make-all-nj for an example |
|
25 using the Bourne shell, sh. |
25 |
26 |
26 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML |
27 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML |
27 images. When using Poly/ML, ISABELLEBIN must be an absolute pathname (one |
28 images. When using Poly/ML, ISABELLEBIN must be an absolute pathname (one |
28 starting with "/"). |
29 starting with "/"). |
29 |
30 |
46 The directory Pure containes pure Isabelle, which has no object-logic. |
47 The directory Pure containes pure Isabelle, which has no object-logic. |
47 |
48 |
48 Other important files include... |
49 Other important files include... |
49 COPYRIGHT Copyright notice and Disclaimer of Warranty |
50 COPYRIGHT Copyright notice and Disclaimer of Warranty |
50 make-all shell script for building entire system |
51 make-all shell script for building entire system |
|
52 make-all-poly sample make-all invocation for Poly/ML |
|
53 make-all-nj sample make-all invocation for SML of NJ |
51 change_simp shell script to help convert sources to new simplifier |
54 change_simp shell script to help convert sources to new simplifier |
52 expandshort shell script to expand "shortcuts" in files |
55 expandshort shell script to expand "shortcuts" in files |
53 prove_goal.el Emacs command to change proof format |
56 prove_goal.el Emacs command to change proof format |
54 xlisten shell script for running Isabelle under X |
57 xlisten shell script for running Isabelle under X |
55 teeinput shell script to run Isabelle, logging inputs to a file |
58 teeinput shell script to run Isabelle, logging inputs to a file |
63 |
66 |
64 The following subdirectories contain object-logics: |
67 The following subdirectories contain object-logics: |
65 FOL Natural deduction First-Order Logic (intuitionistic and classical) |
68 FOL Natural deduction First-Order Logic (intuitionistic and classical) |
66 FOLP First-Order Logic with Proof terms |
69 FOLP First-Order Logic with Proof terms |
67 ZF Zermelo-Fraenkel set theory |
70 ZF Zermelo-Fraenkel set theory |
|
71 HOL Classical Higher-Order Logic |
|
72 LCF Logic for Computable Functions (domain theory) built upon FOL |
|
73 HOLCF A version of LCF built upon HOL |
68 CTT Constructive Type Theory |
74 CTT Constructive Type Theory |
69 HOL Classical Higher-Order Logic |
|
70 LK Classical first-order sequent calculus |
75 LK Classical first-order sequent calculus |
71 Modal The modal logics T, S4, S43 |
76 Modal The modal logics T, S4, S43 |
72 LCF Logic for Computable Functions (domain theory) |
|
73 CCL Martin Coen's Classical Computational Logic |
77 CCL Martin Coen's Classical Computational Logic |
74 Cube Barendregt's Lambda Cube |
78 Cube Barendregt's Lambda Cube |
75 |
79 |
76 Object-logics include examples files in subdirectory ex or file ex.ML. |
80 Object-logics include examples files in subdirectory ex or file ex.ML. |
77 These files can be loaded in batch mode. The commands can also be |
81 These files can be loaded in batch mode. The commands can also be |