equal
deleted
inserted
replaced
31 instantiated for other types and logics as well. |
31 instantiated for other types and logics as well. |
32 |
32 |
33 |
33 |
34 *** General *** |
34 *** General *** |
35 |
35 |
|
36 * improved browser info generation: better HTML markup (including |
|
37 colors), graph views in several sizes; isatool usedir now provides a |
|
38 proper interface for user theories (via -P option); |
|
39 |
36 * theory loader rewritten from scratch (may not be fully |
40 * theory loader rewritten from scratch (may not be fully |
37 bug-compatible); old loadpath variable has been replaced by show_path, |
41 bug-compatible); old loadpath variable has been replaced by show_path, |
38 add_path, del_path, reset_path functions; |
42 add_path, del_path, reset_path functions; new operations such as |
|
43 update_thy, touch_thy, remove_thy (see also isatool doc ref); |
39 |
44 |
40 * in locales, the "assumes" and "defines" parts may be omitted if |
45 * in locales, the "assumes" and "defines" parts may be omitted if |
41 empty; |
46 empty; |
42 |
47 |
43 * new print_mode "xsymbols" for extended symbol support (e.g. genuine |
48 * new print_mode "xsymbols" for extended symbol support (e.g. genuine |
52 |
57 |
53 * improved isatool install: option -k creates KDE application icon, |
58 * improved isatool install: option -k creates KDE application icon, |
54 option -p DIR installs standalone binaries; |
59 option -p DIR installs standalone binaries; |
55 |
60 |
56 * added ML_PLATFORM setting (useful for cross-platform installations); |
61 * added ML_PLATFORM setting (useful for cross-platform installations); |
|
62 more robust handling of platform specific ML images for SML/NJ; |
57 |
63 |
58 * Isamode 2.6 requires patch to accomodate change of Isabelle font |
64 * Isamode 2.6 requires patch to accomodate change of Isabelle font |
59 mode and goal output format: |
65 mode and goal output format: |
60 |
66 |
61 diff -r Isamode-2.6/elisp/isa-load.el Isamode/elisp/isa-load.el |
67 diff -r Isamode-2.6/elisp/isa-load.el Isamode/elisp/isa-load.el |
103 changed syntax and (many) tactics; |
109 changed syntax and (many) tactics; |
104 |
110 |
105 * HOL/typedef: fixed type inference for representing set; type |
111 * HOL/typedef: fixed type inference for representing set; type |
106 arguments now have to occur explicitly on the rhs as type constraints; |
112 arguments now have to occur explicitly on the rhs as type constraints; |
107 |
113 |
108 * HOL/recdef (TFL) now requires theory Recdef; |
114 * HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects |
|
115 comma separated list of theorem names rather than an ML expression; |
109 |
116 |
110 |
117 |
111 *** ZF *** |
118 *** ZF *** |
112 |
119 |
113 * new primrec section allows primitive recursive functions to be given |
120 * new primrec section allows primitive recursive functions to be given |