less frequent sidekick parsing, which is relatively slow;

basic setup for bundled Java runtime;

updated reference platforms;

merged

merged

gave more standard finite set rules simp and intro attribute

more permissive Isabelle_System.mkdir; exported File.is_dir (weak test);

added 'syntax_declaration' command;

more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;

superficial tuning;

updated versions;

recovered Isabelle2009-2 NEWS -- published part is read-only;

follow-up to HOLCF move (cf. 0437dbc127b3, 04d44a20fccf);

removed HOLCF for now as explicit component

fix cut-and-paste errors for HOLCF entries in IsaMakefile

update web description of HOLCF; fix broken link to HOLCF/index.html

remove HOLCF from build script, since it no longer works

moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;

merged

rename Pcpodef.thy to Cpodef.thy; rename pcpodef.ML to cpodef.ML;

renamed several HOLCF theorems (listed in NEWS)

rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo

rename rep_contlub lemmas to rep_lub

rename function 'match_UU' to 'match_bottom'

rename function 'strict' to 'seq', which is its name in Haskell

merged

merged

typscheme with signatures is inappropriate when building empty certificate; prefer logical_typscheme over const_typargs; tuned

merged

merged

corrected: use canonical variables of type scheme uniformly

tuned

merged

consider sort constraints for datatype constructors when constructing the empty equation certificate; actually consider sort constraints in constructor sets; dropped redundant bindings

tuned example

merged

updated generated documents

added equation for Queue; tuned proofs

added evaluation section

tuned formatting; adjustments to changes on ML level

added label

more thorough process termination (cf. Scala version);

prefer Isabelle/ML concurrency elements; more careful propagation of interrupts;

removed bash from ML system bootstrap, and past the Secure ML barrier;

more proper int wrappers;

explicit check for requirement;

more basic Isabelle_System.mkdir;

tuned;

more explicit Isabelle_System operations;

prefer Synchronized.var over CRITICAL/Unsynchronized.ref;

moved file identification to thy_load.ML (where it is actually used);

removed some old settings;

recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);

merged

remove map function names from domain package theory data

isar-style proof for lemma contI2

remove case combinator for fixrec match type

declare more simp rules for powerdomains

merged; adapted ListPair.UnequalLengths;

merged

strict forall2

nbe decides equality of abstractions by extensionality

eliminated some generated comments;

merged

merged

keep type variable arguments of datatype constructors in bookkeeping

document changes in Nitpick and MESON/Metis

renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first

put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs

make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;

just one version of fold_rev2;

explicit use of unprefix;

keep private things private, without comments;

eliminated some clones of eq_list;

merged

new lemma

lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;

prefer non-classical eliminations in Pure reasoning, notably "rule" steps;

discontinued global "Isabelle" symlink, to make each distribution even more self-contained;

more correct spelling;

globbing constant expressions use more idiomatic underscore rather than star

globbing constant expressions use more idiomatic underscore rather than star; precised

datatype constructor glob for code_reflect

merged

merged

merged

toplevel deresolving for flat module name space

merged

Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.

Replace surj by abbreviation; remove surj_on.

adjust Sledgehammer/SMT fudge factor

clarified Par_List.managed_results, with explicit propagation of outermost physical interrupt to forked futures (e.g. to make timeout apply here as expected and prevent zombies);

merge

cosmetics

eta-reduce on the fly to prevent an exception

merged

Added the simplest finite Ramsey theorem

reverted c059d550afec -- the triviality check had apparently nothing to do with spontaneous Interrupt exceptions

set Metis option on correct context, lest it be ignored

make "debug" mode of Sledgehammer/SMT more liberal

fix check for builtinness of 0 and 1 -- these aren't functions

added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway

document requirement on theory import

corrected abd4e7358847 where SOMEthing went utterly wrong

merged

swap names for built-in tester functions (to better reflect the intuition of what they do); eta-expand all built-in functions (even those which are only partially supported)

instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)

more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers

removing Enum.in_enum from the claset

merged

be more precise: only treat constant 'distinct' applied to an explicit list as built-in

be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)

announcing some latest change (d40b347d5b0b)

merged

more precise characterization of built-in constants "number_of", "0", and "1"

merged

merged

adhere established Collect/mem convention more closely

merged

replaced misleading Fset/fset name -- these do not stand for finite sets