derive maps forward

tuning

tuning

provide a mechanism for ensuring dead type variables occur in typedef if desired

preserve order of dead variables

tuning

tuned proofs;

misc tuning and modernization;

misc tuning and modernization;

more simp

msetsum -> set_mset, msetprod -> prod_mset

More on balancing; renamed theory to Balance

added lemmas

option "checkpoint" helps to fine-tune global heap space management;

made it easier to catch 'empty datatype' exception

export ML functions

tuning

minimal HTTP server;

merged

unfold_abs_def is enabled by default;

discontinued theory-local special syntax for lattice orderings

keep locale lifting rules on the global level

tuning

exported ML functions + tuning

refactoring

refactoring

refactoring

tuned whitespace

merged

more operations;

clarified proof: save 1-2s CPU time;

tuned;

strictly sequential abbrevs;

clarified obscure facts;

clarified modules;

clarified modules;

standardized alias;

export more ML functions

generalized ML signature

extended ML signature + refactored

extended ML signature

generalized code (subtly)

tuned ML signature

exported ML functions

export ML function + tuning

tuning multisets; more interpretations

clean argument of simp add

add_mset constructor in multisets

merged

more operations;

more operations; tuned;

support resource management;

clarified modules;

export more ML functions

export more ML functions

added warning

tuned;

tuned signature;

clarified exceptions;

support for (single) primary key; more operations;

more operations; clarified NULL treatment;

more operations;

clarified modules; tuned signature;

tuned;

minimal support for SQLite databases;

merged

make double-sure that refresh happens eventually, even without edits (e.g. height change) -- amending 8bf765c9c2e5;

simplified;

tuned;

merged

added lemmas

consider equality proxy in monotonicity analysis

adapted remote E

Merged

Some facts about factorial and binomial coefficients

added inorder2

tuned headers;

clarified session: use all theories in directory HOL/Library;

clarified session; misc tuning and modernization;

more careful quoting, e.g. relevant for \<^control>cartouche;

uniform capitalization of labels;

tuned message;

merged

avoid conflict after initial keymap migration;

merged

Renamed balanced to complete; added balanced; more about both

tuned GUI: modal dialog last;

tuned message;

merged

NEWS;

more robust persistent storage; tuned;

clarified important directories;

separate action; tuned message;

check keymap changes on startup;

tuned message;

clarified GUI; tuned;

actual actions; tuned;

tuned;

clarified;

tuned GUI;

clarified GUI;

tuned GUI;

tuned rendering;

more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;

clarified shortcut conflicts; tuned;

clarified (see 019856db2bb6, ea52509f4c42);

some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;

added glyph from "Deja Vu Sans Mono" font;

more robustness

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;