enable subpixel anti-aliasing by default, assuming that its 4 variants don't make a difference;

updated to isabelle_fonts-20190210;

recovered missing glyph;

auto-hinting of original DejaVu fonts, but not Isabelle symbols;

tuned signature: proper exports;

more Haskell operations;

Resolved codegen problem with uniformity for formal Laurent series

Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)

Exponentiation by squaring, fast modular exponentiation

more thorough File.set_executable, notably for Windows;

added executable flag for exports; clarified signature;

clarified URL -- avoid odd certificate problem with api.media.atlassian.com;

back to stable polyml-5.7.1-8 for now;

More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots

clarified signature: Path.T as in Generated_Files;

back to polyml-test-1b2dcf8f5202 -- more stable;

updated to polyml-test-b68438d33c69;

clarified default (amending ca9780325a21): it also affects "open-file" dialog, which should be "buffer";

NEWS;

more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";

merged

removed left-over test material (amending bb0a354f6b46);

updated to polyml-test-1236652ebd55;

added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);

adapted to a8ee66876a1a;

show file-browser favorites more prominently: access to Isabelle resources;

tuned -- sort lines;

tuned default layout;

clarified default layout: global overview left, local document information right;

prefer tail-recursive version (despite 4b99b1214034);

proper congruence rule for image operator

less special syntax: make \<Sum> an ordinary function symbol

more robust: avoid crash of browser right-click menu;

more accurate file position;

NEWS;

open session ROOT file;

support for session information via virtual file-system;

clarified modules;

tuned;

tuned signature;

tuned signature;

tuned;

clarified modules;

discontinued obsolete option "checkpoint";

updated to jdk-11.0.2+9;

eliminated suspicious Unicode;

eliminated hard TABs;

merged

moved generalized material

some new results in group theory

less odd class.second_countable_topology_def

revert accident with raw Unicode (not Isabelle symbols) in 7404f5b91e56;

changed precedence of big operators: now like any other function symbol

more canonical and less specialized syntax

updated to polyml-test-1b2dcf8f5202;

prefer proper strings in OCaml

more correct parenthesing

generalized

proper operation in weakly-typed Scala (amending 06153e2e0cdb);

tuned

moved retracts

tagged 4 theories

merged

the theory of Equipollence, and moving Fpow from Cardinals into Main

proper treatment of x86_64_32;

more appropriate section

combinator to lift local theory update to theory update

merged

tagged 5 theories

obsolete -- updated in Poly/ML;

updated to polyml-test-a444f281ccec;

prefer x86_64_32 over x86;

clarified signature;

updated x86_64-linux base line;

fixed me -- indeed this was wrong, as demonstrated by the predicate-free HO output (e.g. ehoh with keep_lams)

tagged 2 theories ie Cartesian_Euclidean_Space Cartesian_Space

minor tagging updates in 13 theories

merged

redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product

Backed out changeset 1bc422c08209 -- obsolete in AFP/5d11846ac6ab;

really keep lambdas in translation if only predicates are missing

tune ATP settings

Added triangular numbers

keep Local_Theory.reset for now -- still required in many AFP sessions (amending 1c201e4792cb);

merged

use polyml-test-0a6ebca445fc by default: already quite stable;

renamings and new material

merged

some renamings and a bit of new material

slightly more conventional naming schema

Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space

updated news

get rid of visibility in MaSh -- it slows it down more than it helps

merged

updated polyml platform: 32=x86_64_32;

more thorough purge_platforms;

clarified ML_OPTIONS on Windows;

more operations;

new material about summations and powers, along with some tweaks

dedicated combinator for declarations nested in a local theory block

more conventional parsing of code_stmts antiquotation

more conventional syntax for code_stmts antiquotation

avoid crash of jEdit.closeBuffer() via TaskManager.instance.waitForIoTasks() due to race condition of save() vs. automatic load() of already open buffer, e.g. relevant for save-as on "isabelle-export:" artifacts;

algebraized more material from theory Divides

tuned output;

more official AFP.groups; clarified bulky sessions;

auto-update for some experimental components;

clarified URLs: prefer sketis over bitbucket;

self-contained code modules for Haskell

automation for unverloading definitions

restore type variable names in unoverload_type

resolved conflict

resolved conflict

tuned headers

amending 689997a8a582

subsection is always %important

no need for %unimportant for proofs of proposition

redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7

revert to 56acd449da41

merge