equal
deleted
inserted
replaced
21 * More robust treatment of structural errors: begin/end blocks take |
21 * More robust treatment of structural errors: begin/end blocks take |
22 precedence over goal/proof. |
22 precedence over goal/proof. |
23 |
23 |
24 * Implicit cases goal1, goal2, goal3, etc. have been discontinued |
24 * Implicit cases goal1, goal2, goal3, etc. have been discontinued |
25 (legacy feature since Isabelle2016). |
25 (legacy feature since Isabelle2016). |
26 |
|
27 |
26 |
28 |
27 |
29 *** HOL *** |
28 *** HOL *** |
30 |
29 |
31 * Simplified syntax setup for big operators under image. In rare |
30 * Simplified syntax setup for big operators under image. In rare |
87 specified in seconds; a negative value means it is disabled (default). |
86 specified in seconds; a negative value means it is disabled (default). |
88 |
87 |
89 * Isabelle Server command "use_theories" terminates more robustly in the |
88 * Isabelle Server command "use_theories" terminates more robustly in the |
90 presence of structurally broken sources: full consolidation of theories |
89 presence of structurally broken sources: full consolidation of theories |
91 is no longer required. |
90 is no longer required. |
|
91 |
|
92 * Support for OCaml via command-line tools "isabelle ocaml_setup", |
|
93 "isabelle ocaml", "isabelle ocamlc", "isabelle ocaml_opam". Existing |
|
94 settings variables ISABELLE_OCAML and ISABELLE_OCAMLC are maintained |
|
95 dynamically according the state of ISABELLE_OPAM_ROOT concerning |
|
96 ISABELLE_OCAML_VERSION. |
92 |
97 |
93 |
98 |
94 |
99 |
95 New in Isabelle2018 (August 2018) |
100 New in Isabelle2018 (August 2018) |
96 --------------------------------- |
101 --------------------------------- |