thread context correctly when printing backquoted facts

dropped dead code; tuned theory text

modernized, simplified and compacted oracle and proof method glue code; corrected slips with poly.Pw and Orderings.less(_eq)

merged

fixed underscores

moved lemmas into projective_family; added header for theory Projective_Family

removed redundant/unnecessary assumptions from projective_family

assume probability spaces; allow empty index set

added projective_family; generalized generator in product_prob_space to projective_family

moved lemmas further up

tuned proofs

using hyp_subst_tac that allows to pass the current simpset to avoid the renamed bound variable warning in the simplifier

hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call

NEWS

rewriting with the simpset that is passed to the simproc

handling x : S y pattern with the default mechanism instead of raising an exception in the set_comprehension_pointfree simproc

tuned

syntactic tuning and restructuring of set_comprehension_pointfree simproc

using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls

improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones

adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs

importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc

handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc

simplified structure of patterns in set_comprehension_simproc

refined stack of library theories implementing int and/or nat by target language numerals

restored SML code check which got unintentionally broken: must explicitly check for error during compilation; restore more conventional namespace during check (relevant for Imperative-HOL)

add support for function application to measurability prover

renamed Sledgehammer option

always show timing for structured proofs

use implications rather than disjunctions to improve readability

avoid name clashes

fixed more "Trueprop" issues

removed needless sort

avoid double "Trueprop"s

use original formulas for hypotheses and conclusion to avoid mismatches

track formula roles in proofs and use that to determine whether the conjecture should be negated or not

correct parsing of E dependencies

proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction

tuned

code for while directly, not via while_option

executable true liveness analysis incl an approximating version

now that sets are executable again, no more special treatment of variable sets

handle non-unit clauses gracefully

several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)

use measurability prover

add measurability prover; add support for Borel sets

add syntax and a.e.-rules for (conditional) probability on predicates

infinite product measure is invariant under adding prefixes

for the product measure it is enough if only one measure is sigma-finite

Allow parentheses around left-hand sides of array associations

made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)

regenerated SMT certificates

regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles

fixed bool vs. prop mismatch

removed "refute" command from Isar manual, now that it has been moved outside "Main"

repaired "Mutabelle" after Refute move