NEWS
changeset 73007 11140980a6b5
parent 72996 cdcd2785db94
child 73008 dacf2598bb27
equal deleted inserted replaced
73006:b60c4ba462d4 73007:11140980a6b5
     6 
     6 
     7 New in Isabelle2021 (February 2021)
     7 New in Isabelle2021 (February 2021)
     8 -----------------------------------
     8 -----------------------------------
     9 
     9 
    10 *** General ***
    10 *** General ***
       
    11 
       
    12 * HTML presentation includes auxiliary files (e.g. ML) for each theory,
       
    13 with rich markup.
    11 
    14 
    12 * Proof method "subst" is confined to the original subgoal range: its
    15 * Proof method "subst" is confined to the original subgoal range: its
    13 included distinct_subgoals_tac no longer affects unrelated subgoals.
    16 included distinct_subgoals_tac no longer affects unrelated subgoals.
    14 Rare INCOMPATIBILITY.
    17 Rare INCOMPATIBILITY.
    15 
       
    16 * HTML presentation includes auxiliary files (e.g. ML) for each theory,
       
    17 with rich markup.
       
    18 
       
    19 
       
    20 *** Isabelle/jEdit Prover IDE ***
       
    21 
       
    22 * Improved markup for theory header imports: hyperlinks for theory files
       
    23 work without formal checking of content.
       
    24 
       
    25 * The prover process can download auxiliary files (e.g. 'ML_file') for
       
    26 theories with remote URL. This requires the external "curl" program.
       
    27 
       
    28 * Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
       
    29 of the formal entity at the caret position.
       
    30 
       
    31 * The visual feedback on caret entity focus is normally restricted to
       
    32 definitions within the visible text area. The keyboard modifier "CS"
       
    33 overrides this: then all defining and referencing positions are shown.
       
    34 See also option "jedit_focus_modifier".
       
    35 
       
    36 * Auto nitpick is enabled by default: it is now reasonably fast due to
       
    37 Kodkod invocation within Isabelle/Scala.
       
    38 
       
    39 * The jEdit status line includes widgets both for JVM and ML heap usage.
       
    40 Ongoing ML ongoing garbage collection is shown as "ML cleanup".
       
    41 
       
    42 * The Monitor dockable provides buttons to request a full garbage
       
    43 collection and sharing of live data on the ML heap. It also includes
       
    44 information about the Java Runtime system.
       
    45 
       
    46 * PIDE support for session ROOTS: markup for directories.
       
    47 
       
    48 * Update to jedit-5.6.0, the latest release. This version works properly
       
    49 on macOS by default, without the special MacOSX plugin.
       
    50 
       
    51 
       
    52 *** Document preparation ***
       
    53 
       
    54 * Keyword 'document_theories' within ROOT specifies theories from other
       
    55 sessions that should be included in the generated document source
       
    56 directory. This does not affect the generated session.tex: \input{...}
       
    57 needs to be used separately.
       
    58 
       
    59 * The standard LaTeX engine is now lualatex, according to settings
       
    60 variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old
       
    61 pdflatex, but text encoding needs to conform strictly to utf8. Rare
       
    62 INCOMPATIBILITY.
       
    63 
       
    64 * Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
       
    65 document output is always PDF.
       
    66 
       
    67 * Antiquotation @{tool} refers to Isabelle command-line tools, with
       
    68 completion and formal reference to the source (external script or
       
    69 internal Scala function).
       
    70 
       
    71 * Antiquotation @{bash_function} refers to GNU bash functions that are
       
    72 checked within the Isabelle settings environment.
       
    73 
       
    74 * Antiquotations @{scala}, @{scala_object}, @{scala_type},
       
    75 @{scala_method} refer to checked Isabelle/Scala entities.
       
    76 
       
    77 
       
    78 *** Pure ***
       
    79 
       
    80 * Session Pure-Examples contains notable examples for Isabelle/Pure
       
    81 (former entries of HOL-Isar_Examples).
       
    82 
       
    83 * Named contexts (locale and class specifications, locale and class
       
    84 context blocks) allow bundle mixins for the surface context.  This
       
    85 allows syntax notations to be organized within bundles conveniently.
       
    86 See src/HOL/ex/Specifications_with_bundle_mixins.thy for examples
       
    87 and the Isar reference manual for syntx descriptions.
       
    88 
       
    89 * Definitions in locales produce rule which can be added as congruence
       
    90 rule to protect foundational terms during simplification.
       
    91 
       
    92 * Consolidated terminology and function signatures for nested targets:
       
    93 
       
    94   * Local_Theory.begin_nested replaces Local_Theory.open_target.
       
    95 
       
    96   * Local_Theory.end_nested replaces Local_Theory.close_target.
       
    97 
       
    98   * Combination of Local_Theory.begin_nested and
       
    99     Local_Theory.end_nested(_result) replaces
       
   100     Local_Theory.subtarget(_result).
       
   101 
       
   102 INCOMPATIBILITY.
       
   103 
       
   104 * Local_Theory.init replaces Generic_Target.init.  Minor INCOMPATIBILITY.
       
   105 
       
   106 
       
   107 *** HOL ***
       
   108 
       
   109 * An updated version of the veriT solver is now included as Isabelle
       
   110 component. It can be used in the "smt" proof method via "smt (verit)" or
       
   111 via "declare [[smt_solver = verit]]" in the context; see also session
       
   112 HOL-Word-SMT_Examples.
       
   113 
       
   114 * Zipperposition 2.0 is included as Isabelle component for
       
   115 experimentation, e.g. in "sledgehammer [prover = zipperposition]".
       
   116 
       
   117 * Nitpick/Kodkod may be invoked directly within the running
       
   118 Isabelle/Scala session (instead of an external Java process): this
       
   119 improves reactivity and saves resources. This experimental feature is
       
   120 guarded by system option "kodkod_scala" (default: true).
       
   121 
       
   122 * Session HOL-Examples contains notable examples for Isabelle/HOL
       
   123 (former entries of HOL-Isar_Examples, HOL-ex etc.).
       
   124 
       
   125 * Simproc "defined_all" and rewrite rule "subst_all" perform more
       
   126 aggressive substitution with variables from assumptions.
       
   127 INCOMPATIBILITY, consider repairing proofs locally like this:
       
   128 
       
   129   supply subst_all [simp del] [[simproc del: defined_all]]
       
   130 
       
   131 * Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
       
   132 on datatypes to "False" if either side is a proper subexpression of the
       
   133 other (for any datatype with a reasonable size function).
       
   134 
       
   135 * New constant "power_int" for exponentiation with integer exponent,
       
   136 written as "x powi n".
       
   137 
       
   138 * Added the "at most 1" quantifier, Uniq.
       
   139 
       
   140 * For the natural numbers, Sup {} = 0.
       
   141 
       
   142 * Updated the Metis prover underlying the "metis" proof method to
       
   143   version 2.4 (release 20180810). The new version fixes one soundness
       
   144   defect and two incompleteness defects. Very slight INCOMPATIBILITY.
       
   145 
       
   146 * Library theory "Bit_Operations" with generic bit operations.
       
   147 
       
   148 * Library theory "Signed_Division" provides operations for signed
       
   149 division, instantiated for type int.
       
   150 
       
   151 * Self-contained library theory "Word" taken over from former session
       
   152 "HOL-Word".
       
   153 
       
   154 * Theory "Word": Type word is restricted to bit strings consisting
       
   155 of at least one bit.  INCOMPATIBILITY.
       
   156 
       
   157 * Theory "Word": Bit operations NOT, AND, OR, XOR are based on
       
   158 generic algebraic bit operations from HOL-Library.Bit_Operations.
       
   159 INCOMPATIBILITY.
       
   160 
       
   161 * Theory "Word": Most operations on type word are set up
       
   162 for transfer and lifting.  INCOMPATIBILITY.
       
   163 
       
   164 * Theory "Word": Generic type conversions.  INCOMPATIBILITY,
       
   165 sometimes additional rewrite rules must be added to applications to
       
   166 get a confluent system again.
       
   167 
       
   168 * Theory "Word": Uniform polymorphic "mask" operation for both
       
   169 types int and word.  INCOMPATIBILITY.
       
   170 
       
   171 * Theory "Word": Syntax for signed compare operators has been
       
   172 consolidated with syntax of regular compare operators.
       
   173 Minor INCOMPATIBILITY.
       
   174 
       
   175 * Former session "HOL-Word": Various operations dealing with bit values
       
   176 represented as reversed lists of bools are separated into theory
       
   177 Reversed_Bit_Lists in session Word_Lib in the AFP.  INCOMPATIBILITY.
       
   178 
       
   179 * Former session "HOL-Word": Theory "Word_Bitwise" has been moved to AFP
       
   180 entry Word_Lib as theory "Bitwise".  INCOMPATIBILITY.
       
   181 
       
   182 * Former session "HOL-Word": Compound operation "bin_split" simplifies
       
   183 by default into its components "drop_bit" and "take_bit".
       
   184 INCOMPATIBILITY.
       
   185 
       
   186 * Former session "HOL-Word": Operations lsb, msb and set_bit are
       
   187 separated into theories Least_significant_bit, Most_significant_bit and
       
   188 Generic_set_bit respectively in session Word_Lib in the AFP.
       
   189 INCOMPATIBILITY.
       
   190 
       
   191 * Former session "HOL-Word": Ancient int numeral representation has been
       
   192 factored out in separate theory "Ancient_Numeral" in session Word_Lib
       
   193 in the AFP.  INCOMPATIBILITY.
       
   194 
       
   195 * Former session "HOL-Word": Operations "bin_last", "bin_rest",
       
   196 "bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and
       
   197 "max_word" are now mere input abbreviations.  Minor INCOMPATIBILITY.
       
   198 
       
   199 * Former session "HOL-Word": Misc ancient material has been factored out
       
   200 into separate theories and moved to session Word_Lib in the AFP.  See
       
   201 theory "Guide" there for further information.  INCOMPATIBILITY.
       
   202 
       
   203 * Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
       
   204 are in working order again, as opposed to outputting "GaveUp" on nearly
       
   205 all problems.
       
   206 
       
   207 * Sledgehammer:
       
   208   - Use veriT in proof preplay.
       
   209   - Take adventage of more cores in proof preplay.
       
   210 
       
   211 * Syntax for state monad combinators fcomp and scomp is organized in
       
   212 bundle state_combinator_syntax.  Minor INCOMPATIBILITY.
       
   213 
       
   214 * Syntax for reflected term syntax is organized in bundle term_syntax,
       
   215 discontinuing previous locale term_syntax.  Minor INCOMPATIBILITY.
       
   216 
       
   217 * Session "HOL-Hoare": concrete syntax only for Hoare triples, not
       
   218 abstract language constructors.
       
   219 
       
   220 * Session "HOL-Hoare": now provides a total correctness logic as well.
       
   221 
       
   222 
       
   223 *** FOL ***
       
   224 
       
   225 * Added the "at most 1" quantifier, Uniq, as in HOL.
       
   226 
       
   227 * Simproc "defined_all" and rewrite rule "subst_all" have been changed
       
   228 as in HOL.
       
   229 
       
   230 
       
   231 *** ML ***
       
   232 
    18 
   233 * Theory_Data extend operation is obsolete and needs to be the identity
    19 * Theory_Data extend operation is obsolete and needs to be the identity
   234 function; merge should be conservative and not reset to the empty value.
    20 function; merge should be conservative and not reset to the empty value.
   235 Subtle INCOMPATIBILITY and change of semantics (due to
    21 Subtle INCOMPATIBILITY and change of semantics (due to
   236 Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
    22 Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
   237 the begin of a new theory can be achieved via Theory.at_begin.
    23 the begin of a new theory can be achieved via Theory.at_begin.
   238 
    24 
       
    25 
       
    26 *** Isabelle/jEdit Prover IDE ***
       
    27 
       
    28 * Improved markup for theory header imports: hyperlinks for theory files
       
    29 work without formal checking of content.
       
    30 
       
    31 * The prover process can download auxiliary files (e.g. 'ML_file') for
       
    32 theories with remote URL. This requires the external "curl" program.
       
    33 
       
    34 * Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
       
    35 of the formal entity at the caret position.
       
    36 
       
    37 * The visual feedback on caret entity focus is normally restricted to
       
    38 definitions within the visible text area. The keyboard modifier "CS"
       
    39 overrides this: then all defining and referencing positions are shown.
       
    40 See also option "jedit_focus_modifier".
       
    41 
       
    42 * Auto nitpick is enabled by default: it is now reasonably fast due to
       
    43 Kodkod invocation within Isabelle/Scala.
       
    44 
       
    45 * The jEdit status line includes widgets both for JVM and ML heap usage.
       
    46 Ongoing ML ongoing garbage collection is shown as "ML cleanup".
       
    47 
       
    48 * The Monitor dockable provides buttons to request a full garbage
       
    49 collection and sharing of live data on the ML heap. It also includes
       
    50 information about the Java Runtime system.
       
    51 
       
    52 * PIDE support for session ROOTS: markup for directories.
       
    53 
       
    54 * Update to jedit-5.6.0, the latest release. This version works properly
       
    55 on macOS by default, without the special MacOSX plugin.
       
    56 
       
    57 
       
    58 *** Document preparation ***
       
    59 
       
    60 * Keyword 'document_theories' within ROOT specifies theories from other
       
    61 sessions that should be included in the generated document source
       
    62 directory. This does not affect the generated session.tex: \input{...}
       
    63 needs to be used separately.
       
    64 
       
    65 * The standard LaTeX engine is now lualatex, according to settings
       
    66 variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old
       
    67 pdflatex, but text encoding needs to conform strictly to utf8. Rare
       
    68 INCOMPATIBILITY.
       
    69 
       
    70 * Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
       
    71 document output is always PDF.
       
    72 
       
    73 * Antiquotation @{tool} refers to Isabelle command-line tools, with
       
    74 completion and formal reference to the source (external script or
       
    75 internal Scala function).
       
    76 
       
    77 * Antiquotation @{bash_function} refers to GNU bash functions that are
       
    78 checked within the Isabelle settings environment.
       
    79 
       
    80 * Antiquotations @{scala}, @{scala_object}, @{scala_type},
       
    81 @{scala_method} refer to checked Isabelle/Scala entities.
       
    82 
       
    83 
       
    84 *** Pure ***
       
    85 
       
    86 * Session Pure-Examples contains notable examples for Isabelle/Pure
       
    87 (former entries of HOL-Isar_Examples).
       
    88 
       
    89 * Named contexts (locale and class specifications, locale and class
       
    90 context blocks) allow bundle mixins for the surface context. This allows
       
    91 syntax notations to be organized within bundles conveniently. See theory
       
    92 "HOL-ex.Specifications_with_bundle_mixins" for examples and the isar-ref
       
    93 manual for syntax descriptions.
       
    94 
       
    95 * Definitions in locales produce rule which can be added as congruence
       
    96 rule to protect foundational terms during simplification.
       
    97 
       
    98 * Consolidated terminology and function signatures for nested targets:
       
    99 
       
   100   - Local_Theory.begin_nested replaces Local_Theory.open_target
       
   101 
       
   102   - Local_Theory.end_nested replaces Local_Theory.close_target
       
   103 
       
   104   - Combination of Local_Theory.begin_nested and
       
   105     Local_Theory.end_nested(_result) replaces
       
   106     Local_Theory.subtarget(_result)
       
   107 
       
   108 INCOMPATIBILITY.
       
   109 
       
   110 * Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY.
       
   111 
       
   112 
       
   113 *** HOL ***
       
   114 
       
   115 * Session HOL-Examples contains notable examples for Isabelle/HOL
       
   116 (former entries of HOL-Isar_Examples, HOL-ex etc.).
       
   117 
       
   118 * An updated version of the veriT solver is now included as Isabelle
       
   119 component. It can be used in the "smt" proof method via "smt (verit)" or
       
   120 via "declare [[smt_solver = verit]]" in the context; see also session
       
   121 HOL-Word-SMT_Examples.
       
   122 
       
   123 * Zipperposition 2.0 is now included as Isabelle component for
       
   124 experimentation, e.g. in "sledgehammer [prover = zipperposition]".
       
   125 
       
   126 * Sledgehammer:
       
   127   - support veriT in proof preplay
       
   128   - take adventage of more cores in proof preplay
       
   129 
       
   130 * Updated the Metis prover underlying the "metis" proof method to
       
   131 version 2.4 (release 20180810). The new version fixes one soundness
       
   132 defect and two incompleteness defects. Very slight INCOMPATIBILITY.
       
   133 
       
   134 * Nitpick/Kodkod may be invoked directly within the running
       
   135 Isabelle/Scala session (instead of an external Java process): this
       
   136 improves reactivity and saves resources. This experimental feature is
       
   137 guarded by system option "kodkod_scala" (default: true).
       
   138 
       
   139 * Simproc "defined_all" and rewrite rule "subst_all" perform more
       
   140 aggressive substitution with variables from assumptions.
       
   141 INCOMPATIBILITY, consider repairing proofs locally like this:
       
   142 
       
   143   supply subst_all [simp del] [[simproc del: defined_all]]
       
   144 
       
   145 * Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
       
   146 on datatypes to "False" if either side is a proper subexpression of the
       
   147 other (for any datatype with a reasonable size function).
       
   148 
       
   149 * Syntax for state monad combinators fcomp and scomp is organized in
       
   150 bundle state_combinator_syntax.  Minor INCOMPATIBILITY.
       
   151 
       
   152 * Syntax for reflected term syntax is organized in bundle term_syntax,
       
   153 discontinuing previous locale term_syntax.  Minor INCOMPATIBILITY.
       
   154 
       
   155 * New constant "power_int" for exponentiation with integer exponent,
       
   156 written as "x powi n".
       
   157 
       
   158 * Added the "at most 1" quantifier, Uniq.
       
   159 
       
   160 * For the natural numbers, "Sup {} = 0".
       
   161 
       
   162 * Library theory "Bit_Operations" with generic bit operations.
       
   163 
       
   164 * Library theory "Signed_Division" provides operations for signed
       
   165 division, instantiated for type int.
       
   166 
       
   167 * Self-contained library theory "Word" taken over from former session
       
   168 "HOL-Word".
       
   169 
       
   170 * Theory "Word": Type word is restricted to bit strings consisting of at
       
   171 least one bit. INCOMPATIBILITY.
       
   172 
       
   173 * Theory "Word": Bit operations NOT, AND, OR, XOR are based on generic
       
   174 algebraic bit operations from HOL-Library.Bit_Operations.
       
   175 INCOMPATIBILITY.
       
   176 
       
   177 * Theory "Word": Most operations on type word are set up for transfer
       
   178 and lifting. INCOMPATIBILITY.
       
   179 
       
   180 * Theory "Word": Generic type conversions. INCOMPATIBILITY, sometimes
       
   181 additional rewrite rules must be added to applications to get a
       
   182 confluent system again.
       
   183 
       
   184 * Theory "Word": Uniform polymorphic "mask" operation for both types int
       
   185 and word. INCOMPATIBILITY.
       
   186 
       
   187 * Theory "Word": Syntax for signed compare operators has been
       
   188 consolidated with syntax of regular compare operators. Minor
       
   189 INCOMPATIBILITY.
       
   190 
       
   191 * Former session "HOL-Word": Various operations dealing with bit values
       
   192 represented as reversed lists of bools are separated into theory
       
   193 Reversed_Bit_Lists in session Word_Lib in the AFP. INCOMPATIBILITY.
       
   194 
       
   195 * Former session "HOL-Word": Theory "Word_Bitwise" has been moved to AFP
       
   196 entry Word_Lib as theory "Bitwise". INCOMPATIBILITY.
       
   197 
       
   198 * Former session "HOL-Word": Compound operation "bin_split" simplifies
       
   199 by default into its components "drop_bit" and "take_bit".
       
   200 INCOMPATIBILITY.
       
   201 
       
   202 * Former session "HOL-Word": Operations lsb, msb and set_bit are
       
   203 separated into theories Least_significant_bit, Most_significant_bit and
       
   204 Generic_set_bit respectively in session Word_Lib in the AFP.
       
   205 INCOMPATIBILITY.
       
   206 
       
   207 * Former session "HOL-Word": Ancient int numeral representation has been
       
   208 factored out in separate theory "Ancient_Numeral" in session Word_Lib in
       
   209 the AFP. INCOMPATIBILITY.
       
   210 
       
   211 * Former session "HOL-Word": Operations "bin_last", "bin_rest",
       
   212 "bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and
       
   213 "max_word" are now mere input abbreviations. Minor INCOMPATIBILITY.
       
   214 
       
   215 * Former session "HOL-Word": Misc ancient material has been factored out
       
   216 into separate theories and moved to session Word_Lib in the AFP. See
       
   217 theory "Guide" there for further information. INCOMPATIBILITY.
       
   218 
       
   219 * Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
       
   220 are in working order again, as opposed to outputting "GaveUp" on nearly
       
   221 all problems.
       
   222 
       
   223 * Session "HOL-Hoare": concrete syntax only for Hoare triples, not
       
   224 abstract language constructors.
       
   225 
       
   226 * Session "HOL-Hoare": now provides a total correctness logic as well.
       
   227 
       
   228 
       
   229 *** FOL ***
       
   230 
       
   231 * Added the "at most 1" quantifier, Uniq, as in HOL.
       
   232 
       
   233 * Simproc "defined_all" and rewrite rule "subst_all" have been changed
       
   234 as in HOL.
       
   235 
       
   236 
       
   237 *** ML ***
       
   238 
   239 * Antiquotations @{scala_function}, @{scala}, @{scala_thread} refer to
   239 * Antiquotations @{scala_function}, @{scala}, @{scala_thread} refer to
   240 registered Isabelle/Scala functions (of type String => String):
   240 registered Isabelle/Scala functions (of type String => String):
   241 invocation works via the PIDE protocol.
   241 invocation works via the PIDE protocol.
   242 
   242 
   243 * Path.append is available as overloaded "+" operator, similar to
   243 * Path.append is available as overloaded "+" operator, similar to
   244 corresponding Isabelle/Scala operation.
   244 corresponding Isabelle/Scala operation.
   245 
   245 
       
   246 * ML statistics via an external Poly/ML process: this allows monitoring
       
   247 the runtime system while the ML program sleeps.
       
   248 
   246 
   249 
   247 *** System ***
   250 *** System ***
       
   251 
       
   252 * Isabelle server allows user-defined commands via
       
   253 isabelle_scala_service.
       
   254 
       
   255 * Update/rebuild external provers on currently supported OS platforms,
       
   256 notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
   248 
   257 
   249 * The command-line tool "isabelle log" prints prover messages from the
   258 * The command-line tool "isabelle log" prints prover messages from the
   250 build database of the given session, following the the order of theory
   259 build database of the given session, following the the order of theory
   251 sources, instead of erratic parallel evaluation. Consequently, the
   260 sources, instead of erratic parallel evaluation. Consequently, the
   252 session log file is restricted to system messages of the overall build
   261 session log file is restricted to system messages of the overall build
   253 process, and thus becomes more informative.
   262 process, and thus becomes more informative.
   254 
   263 
   255 * Update/rebuild external provers on currently supported OS platforms,
       
   256 notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
       
   257 
       
   258 * Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
   264 * Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
   259 variable.
   265 variable.
   260 
   266 
   261 * The command-line tool "isabelle logo" only outputs PDF; obsolete EPS
   267 * The command-line tool "isabelle logo" only outputs PDF; obsolete EPS
   262 (for DVI documents) has been discontinued. Former option -n has been
   268 (for DVI documents) has been discontinued. Former option -n has been
   265 * The shell function "isabelle_directory" (within etc/settings of
   271 * The shell function "isabelle_directory" (within etc/settings of
   266 components) augments the list of special directories for persistent
   272 components) augments the list of special directories for persistent
   267 symbolic path names. This improves portability of heap images and
   273 symbolic path names. This improves portability of heap images and
   268 session databases. It used to be hard-wired for Isabelle + AFP, but
   274 session databases. It used to be hard-wired for Isabelle + AFP, but
   269 other projects may now participate on equal terms.
   275 other projects may now participate on equal terms.
   270 
       
   271 * ML statistics via an external Poly/ML process: this allows monitoring
       
   272 the runtime system while the ML program sleeps.
       
   273 
   276 
   274 * The command-line tool "isabelle process" now prints output to
   277 * The command-line tool "isabelle process" now prints output to
   275 stdout/stderr separately and incrementally, instead of just one bulk to
   278 stdout/stderr separately and incrementally, instead of just one bulk to
   276 stdout after termination. Potential INCOMPATIBILITY for external tools.
   279 stdout after termination. Potential INCOMPATIBILITY for external tools.
   277 
   280 
   319 specified in Isabelle/Scala, as instance of class
   322 specified in Isabelle/Scala, as instance of class
   320 isabelle.Command_Span.Load_Command registered via isabelle_scala_service
   323 isabelle.Command_Span.Load_Command registered via isabelle_scala_service
   321 in etc/settings. This allows more flexible schemes than just a list of
   324 in etc/settings. This allows more flexible schemes than just a list of
   322 file extensions. Minor INCOMPATIBILITY, e.g. see theory
   325 file extensions. Minor INCOMPATIBILITY, e.g. see theory
   323 HOL-SPARK.SPARK_Setup to emulate the old behaviour.
   326 HOL-SPARK.SPARK_Setup to emulate the old behaviour.
   324 
       
   325 * Isabelle server allows user-defined commands via
       
   326 isabelle_scala_service.
       
   327 
   327 
   328 * Isabelle/Phabricator supports Ubuntu 20.04 LTS.
   328 * Isabelle/Phabricator supports Ubuntu 20.04 LTS.
   329 
   329 
   330 * Isabelle/Phabricator setup has been updated to follow ongoing
   330 * Isabelle/Phabricator setup has been updated to follow ongoing
   331 development: libphutil has been discontinued. Minor INCOMPATIBILITY:
   331 development: libphutil has been discontinued. Minor INCOMPATIBILITY: