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