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

less verbose -- the warning will reach the users anyway by other means

tuned messages

moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong

fixes related to Refute's move

added a timeout around script that relies on the network

took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly

moved Refute to "HOL/Library" to speed up building "Main" even more