NEWS
changeset 64529 1c0b93961cb1
parent 64441 cc2da001465b
parent 64527 49708cffb98d
child 64532 fc2835a932d9
     1.1 --- a/NEWS	Thu Nov 24 15:04:05 2016 +0100
     1.2 +++ b/NEWS	Sun Nov 27 20:25:38 2016 +0100
     1.3 @@ -70,6 +70,11 @@
     1.4  
     1.5  *** Prover IDE -- Isabelle/Scala/jEdit ***
     1.6  
     1.7 +* More aggressive flushing of machine-generated input, according to
     1.8 +system option editor_generated_input_delay (in addition to existing
     1.9 +editor_input_delay for regular user edits). This may affect overall PIDE
    1.10 +reactivity and CPU usage.
    1.11 +
    1.12  * Syntactic indentation according to Isabelle outer syntax. Action
    1.13  "indent-lines" (shortcut C+i) indents the current line according to
    1.14  command keywords and some command substructure. Action
    1.15 @@ -99,7 +104,7 @@
    1.16  * Highlighting of entity def/ref positions wrt. cursor.
    1.17  
    1.18  * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
    1.19 -occurences of the formal entity at the caret position. This facilitates
    1.20 +occurrences of the formal entity at the caret position. This facilitates
    1.21  systematic renaming.
    1.22  
    1.23  * PIDE document markup works across multiple Isar commands, e.g. the
    1.24 @@ -910,11 +915,12 @@
    1.25  support for monotonicity and continuity in chain-complete partial orders
    1.26  and about admissibility conditions for fixpoint inductions.
    1.27  
    1.28 -* Session HOL-Library: theory Polynomial contains also derivation of
    1.29 -polynomials but not gcd/lcm on polynomials over fields. This has been
    1.30 -moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to pave
    1.31 -way for a possible future different type class instantiation for
    1.32 -polynomials over factorial rings. INCOMPATIBILITY.
    1.33 +* Session HOL-Library: theory Library/Polynomial contains also
    1.34 +derivation of polynomials (formerly in Library/Poly_Deriv) but not
    1.35 +gcd/lcm on polynomials over fields. This has been moved to a separate
    1.36 +theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible
    1.37 +future different type class instantiation for polynomials over factorial
    1.38 +rings. INCOMPATIBILITY.
    1.39  
    1.40  * Session HOL-Library: theory Sublist provides function "prefixes" with
    1.41  the following renaming