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

tuning

use metaquantification when possible in Isar proofs

tuned code