more theorems concerning gcd/lcm/Gcd/Lcm

further generalization and polishing

pulled out legacy aliasses and infamous dvd interpretations into theory appendix

prefer abbreviations for compound operators INFIMUM and SUPREMUM

consolidated name

merged

removed obsolete RC tags;

merged

Added tag Isabelle2016 for changeset d3996d5873dd

proper syntax;

tuning

making 'pred_inject' a first-class BNF citizen

refactoring

adjust 112eefe85ff0 to 532ad8de5d61

NEWS

correct (apparently untested) e1698a9578ea

document predicator in datatypes

derive transfer rule for predicator

call the predicator of list list_all

document new 'primrec' feature

allow predicator instead of map function in 'primrec'

simp rules for fsts, snds, setl, setr

make predicator a first-class bnf citizen

avoid duplicate theorems in 'primrec's result when invoked programmatically

tuning

keep 'ctor_iff_dtor' theorem around in BNF FP database

tuning

rephrased message

clearer error message

document a limitation of 'primcorec'

use 'undefined' instead of 'Eps'

more explicit dummy proofs;

more explicit dummy proofs;

unused;

command '\<proof>' is an alias for 'sorry', with different typesetting;

more antiquotations;

more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;

tuned whitespace;

more careful quoting for the sake of Windows;

tuned;

tuned;

tuned signature;

more direct invocation of ISABELLE_BASH_PROCESS on Windows;

tuned signature;

tuned signature;

updated bash_process;

actually wait for forked process and return its status -- this is not meant to be a daemon;

tuned signature;

tuned signature -- more like ML version;

suppress empty messages as in ML;

clarified bash process -- similar to ML version;

clarified bash process;

tuned according to ML version;

clarified name;

more flexible command-line; flush before exit/fork/exec, to make double sure that output is shipped;

tuned signature;

isabelle update_cartouches -c -t;

practically obsolete;

obsolete -- no such conditions in main Isabelle repository;

tuned header;

clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;

unconditional test -- nothing special here;

merged

Added tag Isabelle2016-RC5 for changeset 45adb8dc84e1

invoke perl system with explicit list -- to avoid extra /bin/sh and thus evade potential conflict of /bin/sh -> dash with bash on Debian/Ubuntu;

evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged;

tuned;

misc tuning;

misc tuning and updates;

misc tuning and updates;

misc tuning;

tuned whitespace;

more on "Markdown-like text structure";

more on 'consider';

tuned;

more explicit dummy proofs;

misc tuning and updates;

tuned;

clarified old forms;

Added tag Isabelle2016-RC4 for changeset f4baefee5776

tuned proofs;

more on Mac OS X with Retina display;

re-init document views for the sake of Text_Overview size;

removed unused cancel operation;

separate delay_repaint to ensure reactivity, indepently of future_refresh status; clarified delay_refresh: do not cancel already running task, but retry later;

suppress ISABELLE_ROOT after init, to avoid conflict with ISABELLE_HOME when folding file names in "isabelle jedit" command-line tool;

clarified;

recovered handle_resize from 5922db0430f1;

preplaying of 'smt' and 'metis' more in sync with actual method

updated HOL-specific section w.r.t. datatypes

proper markup for formal text;

Added tag Isabelle2016-RC3 for changeset 81cbea2babd9

tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;

more on "ML debugging within the Prover IDE";

updated to official polyml-5.6;

misc tuning and updates;

misc tuning and updates;

misc tuning;

allow single quote within URL;

proper try_run for exactly one evaluation of body (amending 91c3aedbfc5e);

more thorough syntax_changed: new commands need require new folds;

Added tag Isabelle2016-RC2 for changeset 5d513565749e

proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;

clarified exception handling;

guard sessions that no longer work with SML/NJ -- memory problems;

tuned signature; tuned;

tuned;

tuned;

tuned;

proper NEWS for this release;

more CONTRIBUTORS;

tuned;

discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;

back to elementary options used in Isabelle2015 for jdk-7 -- none of the intermediate experiments for jdk-8 improved reactivity on particular dual-CPU system, but the problem seems to be absent on common single-CPU systems;

empty abbrevs are removed globally;

tuned markup, e.g. relevant for Rendering.tooltip;

tuned message;

more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized;

report error on internal channel as well: startup_failure dialog may be too late;

clarified errors: more explicit treatment of uninitialized state;