resolved conflict

more canonical names

more canonical names

more canonical names

merged

merged;

support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);

avoid outdated Process.interruptConsoleProcesses;

tuning

updated doc

tuning

Merge

New and revised material for (multivariate) analysis

was only of historical interest anymore

An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!

generalize more theorems to support enat and ennreal

moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add

Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.

add extended nonnegative real numbers

remove lattice syntax from countable complete lattice

add countable complete lattices

Borel_Space.borel is now in the type class locale

add tendsto_add_ereal_nonneg

add transfer rule for countable

instantiate topologies for nat, int and enat

add type class for topological monoids

move product topology to HOL-Complex_Main

more theorems

sorted out some duplicate fact bindings

more direct bootstrap of char type, still retaining the nibble representation for syntax

moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";

tutorial is old;

tuned

merged

unconditional Multithreading; clarified files;

NEWS concerning 66a381d3f88f

merged

tuned;

clarified file names;

SML/NJ is no longer supported;

dropped various legacy fact bindings and tuned proofs

separated potentially conflicting type class instance into separate theory

gcd instances for poly

more sophisticated GCD syntax

cleansed junk-producing interpretations for gcd/lcm on nat altogether

dropped various legacy fact bindings

generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule

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";