more explicit markup for improper commands; clarified CSS rendering;

tuned;

imitate command markup and rendering of Isabelle/jEdit in HTML output;

tuned signature;

more jEdit colors;

proper alt_string markup (cf. 2ceb05ee0331); more jEdit colors, less PG colors (see bb20fb8a57be);

tuned spelling;

clarified language context, e.g. relevant for symbol completion within cartouches;

tuned signature;

proper railsetup;

move topology on enat to Extended_Real, otherwise Jinja_Threads fails

isatest for Mac OS X Yosemite;

tuned spelling;

expand ML cartouches to Input.source; tuned signature;

merged

some special cases for official SML, to treat Isabelle symbols like raw characters;

tuned comment;

clarified Isabelle/ML strings (refining 72238ea2201c);

tuned signature;

instance bool and enat as topologies

NEWS

allow multiple inheritance of targets

tuned module structure

tuned data structures

tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge; n. b. merging of bidirectional dependencies results in effective join of involved nodes: no termination problem since ancestry is always kept explicitly normalized

tuned

tuned names

eta-expand all search patterns using schematic place holders

revert "better" handling of abbreviation from c61fe520602b

tuned variable names

turn application-specific Pattern.matches_subterm into an application-private function

cleaned up mess

add Poisson and Binomial distribution

add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav

proper GUI_Thread context (cf. 7e0d3da6e6d8);

more examples;

tuned header;

generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces

merged

node-specific keywords, with session base syntax as default;

clarified define_command: send tokens more directly, without requiring keywords in ML;

more robust bundle_name: avoid assumptions about identifier, keywords etc.;

tuned signature;

tuned;

clarified token kind;

added Untyped.method convenience (for *this* class only);

tuned signature -- more explicit types;

more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;

node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;

clarified token marker / syntax for mode vs. buffer;

Sidekick syntax is derived from buffer (and its mode), instead of parser name;

tuned signature;

more merge operations;

tuned signature;

tuned;

prefer E 1.8, now that it's been tried and tested

more accurate context;

update_cartouches;

tuned signature;

tuned signature;

tuned signature -- prefer Input.source;

more abstract type Input.source;

encode text with control symbols;

proper HTML.encode;

prefer abbrev for is_unit

do not conceal inductive predicate names properly, following 4a3747517552

tuned

renamed "pairself" to "apply2", in accordance to @{apply 2};

added ML antiquotation @{apply n} or @{apply n(k)};

even more exception traces for Document.update, which goes through additional execution wrappers;

more informative failure of protocol commands, with exception trace; eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);

load simple_thread.ML later, such that it benefits from redefined print_exception_trace;

tuned proof that pmfs are bnfs

projections of pair_pmf (by D. Traytel)

merged

removed odd remains of structural containment checks, which stem from an older approach (see also 3ad1b289f21b, 3ae3cc4b1eac, 423af2e013b8, bad13b32c0f3, ccd6de95f4a6); de-facto this alternative never occured in practice, but it can lead to non-termination of the check;

preinstantiate (co)inductions in N2M to handle mutual but separated SCCs

add congruence solver to measurability prover

cleanup measurability prover

updated SMT certificates

added one more CVC4 option that helps Judgment Day (10 theory version)

tuned whitespace

keep all 'ctr' theorems

smoothly handle unit codatatypes in 'primcorec'

careful with de Bruijn indices

improved message in 'co' case

updated NEWS

no need for subset operation as a primitive in Nitpick, esp. that its implementation was unsound (cf. Rene Thiemann's 16 Oct 2014 email on isabelle mailing list)

added Z3 reconstruction rule suggested by F. Maric

one more CVC4 option that helps

renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names

update CVC4 version docs

tuned signature;

tuned;

misc tuning and modernization;

misc tuning and modernization;

more careful ML source positions, for improved PIDE markup;

named_theorems: multiple args;

tuned;

removed some add-ons from modules that are relevant for the inference kernel;

add lemma following a proof suggestion by Joachim Breitner

add lemma

register pmf as BNF

added CVC4 option that helps on JD

always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says)

work around bug in CVC4, with boolean arguments to (co)datatypes

other way of crashing (with CVC4)

set right logic for CVC4 with (co)datatypes

removed explicit '--quant-cf' option to CVC4, now that it's the default

more accurate lemma name

parse CVC4 unsat cores

tuning

removed redundant code line

clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;

add reindex rules for distr and nn_integral on count_space

generalized lemmas and tuned proofs

generalized lemmas (particularly concerning dvd) as far as appropriate

formally self-contained gcd type classes

merged

no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";

use \isastyletext directly via 'text' command;

proper sequential version (cf. 302104d8366b);

documentation stubs about permanent_interpretation

cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory

merged

import general theorems from AFP/Markov_Models

uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;

tuning

merged

do not introduce consts too early unnecessarily

added lemma

merged

prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;

make SML/NJ happy;

more careful ML source positions, for improved PIDE markup;

NEWS

tuned proofs

added quickcheck[approximation]

quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}

disjunction and conjunction for forms

truncate intermediate results in horner to improve performance of approximate; more efficient truncated addition float_plus_up/float_plus_down

added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction

cancel real of power of numeral also for equality and strict inequality; simplify floor of power of numeral; lemmas about real/floor

simplified computations based on round_up by reducing to round_down; more general round_up_le1, round_up_less1, round_down_ge1, round_up_le0

code equation for powr

merged

more careful ML source positions, for improved PIDE markup;

more position information, e.g. relevant for errors in generated ML source;

more symbols;

tuned whitespace;

more markup;

simplifie sessions;

more Isar proof methods;

more Isar proof methods;

more Isar proof methods;

add forgotten lemma

added lemma

make 'corec_transfer' tactic more robust

also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables

make 'rec_transfer' tactic more robust

add del option to measurable; make measurability rules available as dynamic theorem;

merged

proper context for assume_tac (atac remains as fall-back without context);

even -> evn because even is now in Main

dropped redundant transfer rules (now proved and registered by datatype and plugins)

proper context for typedef;

proper proof context for typedef;

proper context;

proper context for match_tac etc.;

proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);

avoid erule and rotated in IMP

reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility

self-contained simp rules for dvd on numerals

equivalence rules for structures without zero divisors

removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);

optional proof context for unify operations, for the sake of proper local options;

clarified name of Type.unified, to emphasize its connection to the "unify" family; tuned low-level operation;

proper Envir.norm_type for result of Type.raw_unifys;

avoid slow metis proof;

proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);

tuned;

updated some sledgehammer proofs -- much faster;

updated sledgehammer proof after breakdown of metis (exception Type.TUNIFY);

recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54); NB: "match" operates on direct substitution without variable chasing, in contrast to "unify" (and Unify.matches!) which work on cascaded env;

more direct type equality;

reverted commit accident from 994fe0ba8335

less space-wasting serialization setup: highest cell of array has been unused so far

tuned outline;

tuned syntax -- separate tokens;

eliminated pointless check -- command definitions are subject to theory context;

merged

prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors; tuned message;

tuned markup;

tuned;

clarified keyword categories; tuned;

tuned signature;

tuned;

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

proper import for command 'permanent_interpretation';

proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;

more accurate keywords;

tuned signature;

more explicit Keyword.keywords;

proper Keyword.keywords (cf. 82a71046dce8);

prefer explicit Keyword.keywords (cf. 82a71046dce8);

tuned signature;

prefer explicit Keyword.keywords;

simplified keyword kinds; more explicit bootstrap syntax;

Tidying up. Removing unnecessary conditions from some theorems.

more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories

document '*_transfer' attribute

document 'size_neq'

generate 'size_neq' for datatypes

fix 'unfla' function

proper oriented equivalence of dvd predicate and mod

merged

more symbols;

tuned signature;

more uniform header_keywords in ML/Scala; tuned signature;

tuned;

more frugal keywords;

eliminated pointless dynamic keywords (TTY legacy);

explicit type Keyword.keywords; tuned signature;

tuned;

clarified representation of type Keywords; tuned signature;

explicit type Keyword.Keywords;

clarified minor/major lexicon (like ML version);

reduced execution time

proper button margins for Nimbus L&F; properties are sorted when saved;

approximative update of versions;

Added Option.bind_split{,_asm,s}

clarified legacy code;

eliminated unused int_only flag (see also c12484a27367); just proper commands;

eliminated obsolete Proof.goal_message -- print outcome more directly;

updated to scala-2.11.4;

less ambitious isatest: polyml-5.3.0 has problems with big sessions like HOL-Proofs;

modernized header uniformly as section;

prefer \setisabellecontext;

modernized header;

modernized header;