more informative spec rules: optional name;
clarified signature;
more thorough treatment of Thm.trim_context vs. Thm.transfer;

clarified signature: avoid direct comparison on type rough_classification;

isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

tuned signature: more operations;

better duplicate detection

tuned signature;

tuning

position information for literal facts;
Markup.entry may have empty kind/name;

tuned signature -- clarified modules;

--HG--
rename : src/Pure/Concurrent/time_limit.ML => src/Pure/Concurrent/timeout.ML

tuned signature;

more uniform treatment of package internals;

renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;

use cartouches instead of backquotes

speed up MaSh duplicate check

trim context for persistent storage;

prefer theory_id operations;
tuned signature;

clarified context;

tuned signature;

tuned signature, in accordance to sortBy in Scala;

support for 'consider' command;
allow full "fixes" for 'obtain' command;
tuned signature;

improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')

proper context for Object_Logic operations;

tuned;

tuned signature;

more position information;

tuned signature -- prefer qualified names;

tuned signature;

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

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;

prefer explicit Keyword.keywords;

never include hidden names -- these cannot be referenced afterward

gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)

tuned signature -- moved type src to Token, without aliases;

reordered some (co)datatype property names for more consistency

updated to named_theorems;

added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'

whitespace tuning

whitespace tuning

remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer

generate backquotes without markup, since this confuses preplay; bump up spying version identifier;

more generous max number of suggestions, for more safety

more qualified names;

more explicit treatment of verbose mode, which includes concealed entries;

back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;

just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
more thorough background_notes: distribute global notes to all contexts;

clarified Args.check_src: retain name space information for error output;
tuned signature;

prefer Name_Space.pretty with its builtin markup;

tuned signature;

tuning

tuning

tuned signature;

explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;

removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)

tuning

make sure add: doesn't add duplicates, and works for [no_atp] facts

no fact subsumption -- this only confuses later code, e.g. 'add:'

drop only real duplicates, not subsumed facts -- this confuses MaSh

normalize more equalities

added TODO

crank up limit a bit -- truly huge background theories are still nearly 3 times larger

minor fact filter speedups

more gracefully handle huge theories in relevance filters

further optimization in relevance filter

further speed up duplicate elimination

more efficient theorem variable normalization

strengthen top sort check

encode goal digest in spying log (to detect duplicates)

reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently

tuning

disable some checks for huge background theories

tuning

reintroduced half of f99ee3adb81d -- that part definitely looks useless (and is inefficient)

reverted f99ee3adb81d -- that old logic seems to make a difference still today

faster detection of tautologies

slight speed optimization

got rid of another slowdown factor in relevance filter

removed completely needless, inefficient code

minor speed optimization

got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)

avoid double traversal of term

got rid of old, needless logic

faster uniquification

stronger fact normalization

gracefully handle huge thys

speed up detection of simp rules

tuning -- renamed '_from_' to '_of_' in Sledgehammer

renamed Sledgehammer functions with 'for' in their names to 'of'

systematic conversions between nat and nibble/char;
more uniform approaches to execute operations on nibble/char

--HG--
extra : rebase_source : 982810ecce9e31070e2293715ed744c3b68ae21d

reform of predicate compiler / quickcheck theories:
implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers!
avoid odd New_ prefix by joining related theories;
avoid overcompact name DSequence;
separated predicate inside random monad into separate theory;
consolidated name of theory Quickcheck

--HG--
rename : src/HOL/DSequence.thy => src/HOL/Limited_Sequence.thy
rename : src/HOL/Quickcheck.thy => src/HOL/Quickcheck_Random.thy
extra : rebase_source : b6adaac1637d6d1cc809d2f937ae890fcc21969c

distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds

make name table work the way it was intended to

put single-theorem names before multi-theorem ones (broken since 5d147d492792)

tuned blacklisting in relevance filter

refined class handling, to prevent cycles in fact graph

learn from low-level, inside-class facts

tuning

add a timeout in induction rule instantiation

get rid of some junk facts in the MaSh evaluation driver

tweaked which facts are included for MaSh evaluations

don't query blacklisted theorems in evaluation driver

export a pair of ML functions

further fix related to bd9a0028b063 -- that change was per se right, but it exposed a bug in the pattern for "all"

better tautology check -- don't reject "prod_cases3" for example

really all facts means really all facts (well, almost)

merge aliased theorems in MaSh dependencies, modulo symmetry of equality

push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)

don't blacklist "case" theorems -- this causes problems in MaSh later

tuned signature;
tuned;

fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies

avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit

centralized term printing code

thread context correctly when printing backquoted facts

tuning

rule out same "technical" theories for MePo as for MaSh

repaired accessibility chains generated by MaSh exporter + tuned one function out

identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway

distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh

tuning

honor suggested MaSh weights

minimal maxes + tuning

name tuning

fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully

optimize parent computation in MaSh + remove temporary files

don't include hidden facts in relevance filter + tweak MaSh learning

centrally construct expensive data structures

more work on MaSh

gracefully handle the case of empty theories when going up the accessibility chain

more code rationalization in relevance filter

moved most of MaSh exporter code to Sledgehammer

further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)