added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)

make workaround possible for Quickcheck with nesting

tuned docs

tuned final stop in message

generate proper goal when equation is entered programmatically

clarified default;

Bohr-Mollerup theorem for the Gamma function

Back to original example theorem.

Improved error reporting when activating a locale instance.

Deprivatisation of lemmas in Polynomial_Factorial

More analysis lemmas

added lemma

tuned signature

replaced the confusing int parameter by bool

remove spurious find_theorems

HOL-Probability: Projective_Limit was missing (cf. 44ce6b524ff3); tuned

removed debug output

derive pred_mono property for BNFs

Tuned L'Hospital

merged

more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay

merged

coinduction method accepts a list of coinduction rules (takes the first matching one)

more robust;

clarified presentation order, according to typical amounts;

present ML timing as well;

Polynomial algebra cleanup (tuned)

Polynomial algebra cleanup

provide index.html; tuned;

cpu time is optional (see Timing.message_resources);

proper display of "_";

clarified options and arguments; tuned;

updated NEWS

optimized parent computation in MaSh

avoid loading MaSh file first time around for higher responsiveness of Sledgehammer

tuned MaSh's metacharacters to avoid needless decoding

optimization in MaSh parsing

tuned ML

removed trailing final stops in Nitpick messages

killed final stops in Sledgehammer and friends

tuned message

tuning punctuation in messages output by Isabelle

tuning whitespace in output syntax

gnuplot presentation similar to former isatest-statistics;

tuned;

statistics from session build output;

more uniform output;

added [simp] lemmas

more robust HTML rendering of hidden control symbols: Vacuous font bypasses minimal font-size restrictions of common browsers, transparent colour imitates hidden visibility while copy-paste still works;

merged

active jEdit actions;

more symbols;

clarified syntax;

updated;

some icons from Symbola font;

more latex symbols, notably for embedded ML;

uniform ML and document antiquotations;

proper completion of path cartouche (amending 5a7c919a4ada);

clarified error;

more uniform path syntax (like url);

liberal name as in document antiquotations;

tuned;

clarified antiquotations;

tuned error;

tuned whitespace;

suppress ASCII art;

added lemma

tuned

Extracted floorlog and bitlen to separate theory Log_Nat

lists form a monoid

formal passive interpretation proofs for conj and disj

add monotonicity propertyies of `mult1` and `mult`

keeping lifting rules local

epheremal interpretation keeps auxiliary definition localized

tuned order of declarations and proofs

tuned

simplified theory hierarchy;

misc tuning and modernization;

misc tuning and modernization;

misc tuning and modernization;

merged

"split add" -> "split". Documented new modifier "split!"

tuned proofs;

"split add" -> "split"

merged

API for Isabelle Jenkins continuous integration services;

more operations;

support for JSON parsing;

New theory Balance_List

more operations;

merged;

print name in parsable form;

clarified bootstrap;

merged

adapted ZF,FOL,CCL,LCF to modified splitter

introduced aggressive splitter "split!"