equal
deleted
inserted
replaced
55 (likewise for "isabelle vscode_server -S"). Existing option "-R" is both |
55 (likewise for "isabelle vscode_server -S"). Existing option "-R" is both |
56 sufficient and more convenient to start editing a particular session. |
56 sufficient and more convenient to start editing a particular session. |
57 |
57 |
58 |
58 |
59 *** HOL *** |
59 *** HOL *** |
|
60 |
|
61 * Term_XML.Encode/Decode.term uses compact representation of Const |
|
62 "typargs" from the given declaration environment. This also makes more |
|
63 sense for translations to lambda-calculi with explicit polymorphism. |
|
64 INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special |
|
65 applications. |
60 |
66 |
61 * ASCII membership syntax concerning big operators for infimum and |
67 * ASCII membership syntax concerning big operators for infimum and |
62 supremum is gone. INCOMPATIBILITY. |
68 supremum is gone. INCOMPATIBILITY. |
63 |
69 |
64 * Clear distinction between types for bits (False / True) and Z2 (0 / |
70 * Clear distinction between types for bits (False / True) and Z2 (0 / |
95 potentially indexed, such as "foo" for singleton facts, or "bar(1)", |
101 potentially indexed, such as "foo" for singleton facts, or "bar(1)", |
96 "bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now |
102 "bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now |
97 exported as well: this spans an overall dependency graph of internal |
103 exported as well: this spans an overall dependency graph of internal |
98 inferences; it might help to reconstruct the formal structure of theory |
104 inferences; it might help to reconstruct the formal structure of theory |
99 libraries. See also the module Export_Theory in Isabelle/Scala. |
105 libraries. See also the module Export_Theory in Isabelle/Scala. |
|
106 |
100 |
107 |
101 |
108 |
102 New in Isabelle2019 (June 2019) |
109 New in Isabelle2019 (June 2019) |
103 ------------------------------- |
110 ------------------------------- |
104 |
111 |