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

tuning

use metaquantification when possible in Isar proofs

tuned code

tuning

soft SMT timeout

added function store_termination_rule to the signature, as it is used in Nominal2

longer log, to accomodate final status line of isabelle build;

transfer package: error message if preprocessing goal to object-logic formula fails

transfer package: add test to prevent trying to make cterms from open terms

transfer package: more flexible handling of equality relations using is_equality predicate

ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta

new theorems

incorporated constant chars into instantiation proof for enum; tuned proofs for properties on enum of chars; swapped theory dependency of Enum.thy and String.thy

close code theorems explicitly after preprocessing

tuned proofs;

further attempts to cope with large files via option jedit_text_overview_limit;

more detailed Prover IDE NEWS;

recovered explicit error message, which was lost in b8570ea1ce25;

removed dead code;

proper signatures;

tuned;

merged

Renamed {left,right}_distrib to distrib_{right,left}.

Tuned.

more conventional argument order; dropped dead code

another refinement in the comprehension conversion

refined simplifier call in comprehension_conv

passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls

avoid STIX font, which tends to render badly;

extra jar for scala-2.10.0-RC1;

more explicit auxiliary classes to avoid warning "reflective access of structural type member method" of scala-2.10.0-RC1;

avoid duplicate build of jars_fresh;

obsolete, cf. README_REPOSITORY;

accomodate scala-2.10.0-RC1;

tailored enum specification towards simple instantiation; tuned enum instantiations

refined internal structure of Enum.thy

moved quite generic material from theory Enum to more appropriate places

adding another test case for the set_comprehension_simproc to the theory in HOL/ex

improving tactic in setcomprehension_simproc

adjusting proofs

tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage

passing names and types of all bounds around in the simproc

locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree

more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;

merged

don't include Quotient_Option - workaround to a transfer bug

ignore old stuff and thus speed up the script greatly;

proper find -mtime (file data) instead of -ctime (meta data);

made SML/NJ happy;

clarified Future.map (again): finished value is mapped in-place, which saves task structures and changes error behaviour slightly (tolerance against canceled group of old value etc.);

back to polyml-5.4.1 (cf. b3110dec1a32) -- no cause of spurious interrupts;

merged

back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;

more basic Goal.reset_futures as snapshot of implicit state; more robust Session.finish_futures: do not cancel here, to allow later Future.map of persistent futures (notably proof terms);

tuned proof;

update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer

tuned proofs

new theorem

merged

merged

merged

merged

fixed proof (cf. a81f95693c68);

tuned Isar output

tuned

updated docs

renamed Isar-proof related options + changed semantics of Isar shrinking

tuning

fixed theorem lookup code in Isar proof reconstruction

tuning

refactor code

tuning

more robust future_proof result with specific error message (e.g. relevant for incomplete proof of non-registered theorem);

collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);

more uniform group for map_future, which is relevant for cancel in worker_task vs. future_job -- prefer peer group despite 81d03a29980c;

tuned message;

tuned comment;

avoid spurious "bad" markup for show/test_proof; tuned;

more official Future.terminate; tuned signature;

simp results for simplification results of Inf/Sup expressions on bool; tuned proofs

no sort constraints on datatype constructors in internal bookkeeping

HOL-BNF-Examples is sequential for now, due to spurious interrupts (again);

merged

comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic

checking for bound variables in the set expression; handling negation more generally