tuned;

support 'for' fixes in rule_tac etc.;

fix parameter order of NO_MATCH

add measurable_submarkov

BT subsumed by Library/Tree

added funs and lemmas

tuned;

tuned;

tuned;

tuned;

read instantiations uniformly for rules and tactics; tuned;

removed presumably pointless detail;

tuned;

tuned;

make SML/NJ happy;

Merge

tweaked a few slow or very ugly proofs

merged

tuned signature;

tuned;

tuned signature;

tuned;

tuned -- prepare instantiation more uniformly;

Merge

fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat!

merged

more position information;

misc tuning;

tuned;

Merge

New material for complex sin, cos, tan, Ln, also some reorganisation

updated to sumatra_pdf-3.0;

tuned comments;

slightly more formal historic examples;

bounded powerset

new HOL Light material about exp, sin, cos

new file for complex transcendental functions

Merge

Merge

Merge

Lots of new material on complex-valued functions. Modified simplification of (x/n)^k

merged

added proof method rewrite

merged

tuned;

tight span for theory header, which is relevant for error positions (including semantic completion);

misc tuning and simplification;

Inserted real_of_nat to fix factorial-related problem

more general type class for factorial. Now allows code generation (?)

Merge

Merge

The factorial function, "fact", now has type "nat => 'a"

merged

added lemmas

document property

BNF relators preserve reflexivity

export more ML functions

merged

suppress semantic completion in errors of batch build -- avoid junk in log files;

updated docs

clarified documentation

proper headers;

merged

tuned message -- include completion;

support for completion reports produced in Scala (inlined into messages);

more precises positions; more permissive imports;

avoid duplicate header errors, more precise positions; tuned signature;

tuned protocol -- resolve command positions in ML;

clarified modules;

add inequalities (move from AFP/Amortized_Complexity)

merge

inlining threshold

avoid controversial Pirate syntax

more markup, which helps to create missing imports;

tuned signature;

proper command id for inlined errors, which is important for Command.State.accumulate;

clarified span position;

tuned;

tuned;

hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;

more command categories, as in ML; tuned;

more command categories, as in ML;

tuned;

value-oriented user error, for well-defined Thy_Syntax.chop_common;

more explicit exception User_Error, with value-oriented equality;

tuned signature;

clarified positions of theory imports;

misc tuning -- more uniform ML vs. Scala;

tunes signature -- more uniform ML vs. Scala;

position parser as in ML;

tuned signature; minimal I/O on GUI thread should be OK;

rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed

simplified Command.resolve_files in ML, using blobs_index from Scala; clarified modules;

removed junk;

tuned;

merged

clarified markup for embedded files, early before execution;

clarified command content;

tuned -- more uniform ML vs. Scala;

quote "method" to allow Eisbach using this keyword;

rel_pmf on equivalence relation

make proofs work with 4762c690a75c

add subadditivity for Liminf on ereal

merged

merged

more type class instances

documented renamed theories

export more functions (for future 'corec')

tuning

merged

more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;

generalized bind_cond_pmf_cancel

renaming HOL/Fact.thy -> Binomial.thy

Merge

Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy

clarified Token.check_src: intern at most once; Method.parse_internal for Eisbach: intern method names;

add set_pmf lemmas to simpset

build pmf's on bind

split into subgoals

tuning