2012-11-02 hoelzl 2012-11-02 add measurability prover; add support for Borel sets
2012-11-02 hoelzl 2012-11-02 add syntax and a.e.-rules for (conditional) probability on predicates
2012-11-02 hoelzl 2012-11-02 infinite product measure is invariant under adding prefixes
2012-11-02 hoelzl 2012-11-02 for the product measure it is enough if only one measure is sigma-finite
2012-11-02 berghofe 2012-11-02 Allow parentheses around left-hand sides of array associations
2012-11-01 blanchet 2012-11-01 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)
2012-11-01 blanchet 2012-11-01 regenerated SMT certificates
2012-11-01 blanchet 2012-11-01 regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
2012-10-31 blanchet 2012-10-31 fixed bool vs. prop mismatch
2012-10-31 blanchet 2012-10-31 removed "refute" command from Isar manual, now that it has been moved outside "Main"
2012-10-31 blanchet 2012-10-31 repaired "Mutabelle" after Refute move
2012-10-31 blanchet 2012-10-31 less verbose -- the warning will reach the users anyway by other means
2012-10-31 blanchet 2012-10-31 tuned messages
2012-10-31 blanchet 2012-10-31 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
2012-10-31 blanchet 2012-10-31 fixes related to Refute's move
2012-10-31 blanchet 2012-10-31 added a timeout around script that relies on the network
2012-10-31 blanchet 2012-10-31 took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly
2012-10-31 blanchet 2012-10-31 moved Refute to "HOL/Library" to speed up building "Main" even more
2012-10-31 blanchet 2012-10-31 tuning
2012-10-31 blanchet 2012-10-31 use metaquantification when possible in Isar proofs
2012-10-31 blanchet 2012-10-31 tuned code
2012-10-31 blanchet 2012-10-31 tuning
2012-10-31 blanchet 2012-10-31 soft SMT timeout
2012-10-28 Christian Urban 2012-10-28 added function store_termination_rule to the signature, as it is used in Nominal2
2012-10-27 wenzelm 2012-10-27 longer log, to accomodate final status line of isabelle build;
2012-10-24 huffman 2012-10-24 transfer package: error message if preprocessing goal to object-logic formula fails
2012-10-24 huffman 2012-10-24 transfer package: add test to prevent trying to make cterms from open terms
2012-10-24 huffman 2012-10-24 transfer package: more flexible handling of equality relations using is_equality predicate
2012-10-24 nipkow 2012-10-24 ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta
2012-10-22 kuncar 2012-10-22 new theorems
2012-10-22 haftmann 2012-10-22 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
2012-10-22 haftmann 2012-10-22 close code theorems explicitly after preprocessing
2012-10-22 wenzelm 2012-10-22 tuned proofs;
2012-10-22 wenzelm 2012-10-22 further attempts to cope with large files via option jedit_text_overview_limit;
2012-10-22 wenzelm 2012-10-22 more detailed Prover IDE NEWS;
2012-10-21 wenzelm 2012-10-21 recovered explicit error message, which was lost in b8570ea1ce25;
2012-10-21 wenzelm 2012-10-21 removed dead code;
2012-10-21 wenzelm 2012-10-21 proper signatures;
2012-10-21 wenzelm 2012-10-21 tuned;
2012-10-21 webertj 2012-10-21 merged
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-19 webertj 2012-10-19 Tuned.
2012-10-21 haftmann 2012-10-21 more conventional argument order; dropped dead code
2012-10-21 bulwahn 2012-10-21 another refinement in the comprehension conversion
2012-10-21 bulwahn 2012-10-21 refined simplifier call in comprehension_conv
2012-10-21 bulwahn 2012-10-21 passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
2012-10-20 wenzelm 2012-10-20 avoid STIX font, which tends to render badly;
2012-10-20 wenzelm 2012-10-20 extra jar for scala-2.10.0-RC1;
2012-10-20 wenzelm 2012-10-20 more explicit auxiliary classes to avoid warning "reflective access of structural type member method" of scala-2.10.0-RC1;
2012-10-20 wenzelm 2012-10-20 avoid duplicate build of jars_fresh;
2012-10-20 wenzelm 2012-10-20 obsolete, cf. README_REPOSITORY;
2012-10-20 wenzelm 2012-10-20 accomodate scala-2.10.0-RC1;
2012-10-20 haftmann 2012-10-20 tailored enum specification towards simple instantiation; tuned enum instantiations
2012-10-20 haftmann 2012-10-20 refined internal structure of Enum.thy
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-10-20 bulwahn 2012-10-20 adding another test case for the set_comprehension_simproc to the theory in HOL/ex
2012-10-20 bulwahn 2012-10-20 improving tactic in setcomprehension_simproc
2012-10-20 bulwahn 2012-10-20 adjusting proofs
2012-10-20 bulwahn 2012-10-20 tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
2012-10-20 bulwahn 2012-10-20 passing names and types of all bounds around in the simproc