2012-11-06 blanchet 2012-11-06 renamed Sledgehammer option
2012-11-06 blanchet 2012-11-06 always show timing for structured proofs
2012-11-06 blanchet 2012-11-06 use implications rather than disjunctions to improve readability
2012-11-06 blanchet 2012-11-06 avoid name clashes
2012-11-06 blanchet 2012-11-06 fixed more "Trueprop" issues
2012-11-06 blanchet 2012-11-06 removed needless sort
2012-11-06 blanchet 2012-11-06 avoid double "Trueprop"s
2012-11-06 blanchet 2012-11-06 use original formulas for hypotheses and conclusion to avoid mismatches
2012-11-06 blanchet 2012-11-06 track formula roles in proofs and use that to determine whether the conjecture should be negated or not
2012-11-06 blanchet 2012-11-06 correct parsing of E dependencies
2012-11-06 blanchet 2012-11-06 proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
2012-11-05 nipkow 2012-11-05 tuned
2012-11-04 nipkow 2012-11-04 code for while directly, not via while_option
2012-11-04 nipkow 2012-11-04 executable true liveness analysis incl an approximating version
2012-11-04 nipkow 2012-11-04 now that sets are executable again, no more special treatment of variable sets
2012-11-02 blanchet 2012-11-02 handle non-unit clauses gracefully
2012-11-02 blanchet 2012-11-02 several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
2012-11-02 hoelzl 2012-11-02 use measurability prover
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.