summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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