2010-11-26 haftmann 2010-11-26 globbing constant expressions use more idiomatic underscore rather than star
2010-11-26 haftmann 2010-11-26 globbing constant expressions use more idiomatic underscore rather than star; precised
2010-11-26 haftmann 2010-11-26 datatype constructor glob for code_reflect
2010-11-26 haftmann 2010-11-26 merged
2010-11-26 haftmann 2010-11-26 merged
2010-11-25 haftmann 2010-11-25 merged
2010-11-25 haftmann 2010-11-25 toplevel deresolving for flat module name space
2010-11-26 hoelzl 2010-11-26 merged
2010-11-23 hoelzl 2010-11-23 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
2010-11-22 hoelzl 2010-11-22 Replace surj by abbreviation; remove surj_on.
2010-11-26 blanchet 2010-11-26 adjust Sledgehammer/SMT fudge factor
2010-11-25 wenzelm 2010-11-25 clarified Par_List.managed_results, with explicit propagation of outermost physical interrupt to forked futures (e.g. to make timeout apply here as expected and prevent zombies);
2010-11-25 blanchet 2010-11-25 merge
2010-11-25 blanchet 2010-11-25 cosmetics
2010-11-25 blanchet 2010-11-25 eta-reduce on the fly to prevent an exception
2010-11-25 nipkow 2010-11-25 merged
2010-11-25 nipkow 2010-11-25 Added the simplest finite Ramsey theorem
2010-11-25 blanchet 2010-11-25 reverted c059d550afec -- the triviality check had apparently nothing to do with spontaneous Interrupt exceptions
2010-11-25 blanchet 2010-11-25 set Metis option on correct context, lest it be ignored
2010-11-25 blanchet 2010-11-25 make "debug" mode of Sledgehammer/SMT more liberal
2010-11-25 blanchet 2010-11-25 fix check for builtinness of 0 and 1 -- these aren't functions
2010-11-25 blanchet 2010-11-25 added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway
2010-11-24 blanchet 2010-11-24 document requirement on theory import
2010-11-24 haftmann 2010-11-24 corrected abd4e7358847 where SOMEthing went utterly wrong
2010-11-24 boehmes 2010-11-24 merged
2010-11-24 boehmes 2010-11-24 swap names for built-in tester functions (to better reflect the intuition of what they do); eta-expand all built-in functions (even those which are only partially supported)
2010-11-24 boehmes 2010-11-24 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
2010-11-24 blanchet 2010-11-24 more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
2010-11-24 bulwahn 2010-11-24 removing Enum.in_enum from the claset
2010-11-24 boehmes 2010-11-24 merged
2010-11-24 boehmes 2010-11-24 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-24 boehmes 2010-11-24 be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
2010-11-24 bulwahn 2010-11-24 announcing some latest change (d40b347d5b0b)
2010-11-23 blanchet 2010-11-23 merged
2010-11-23 blanchet 2010-11-23 more precise characterization of built-in constants "number_of", "0", and "1"
2010-11-23 haftmann 2010-11-23 merged
2010-11-22 haftmann 2010-11-22 merged
2010-11-22 haftmann 2010-11-22 adhere established Collect/mem convention more closely
2010-11-22 haftmann 2010-11-22 merged
2010-11-22 haftmann 2010-11-22 replaced misleading Fset/fset name -- these do not stand for finite sets
2010-11-22 haftmann 2010-11-22 renamed slightly ambivalent crel to effect
2010-11-23 blanchet 2010-11-23 disable triviality checking -- it might be the source of the spurious Interrupt exceptions that make it almost impossible to run Judgement Day
2010-11-23 blanchet 2010-11-23 more precise error handling for Z3; refactored some of the error handling code shared by ATP and SMT
2010-11-23 blanchet 2010-11-23 use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on
2010-11-23 blanchet 2010-11-23 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
2010-11-23 blanchet 2010-11-23 try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
2010-11-23 blanchet 2010-11-23 added "verbose" option to Metis to shut up its warnings if necessary
2010-11-22 boehmes 2010-11-22 added support for quantifier weight annotations
2010-11-22 boehmes 2010-11-22 share and use more utility functions; slightly reduced complexity for Z3 proof rule 'rewrite'
2010-11-22 boehmes 2010-11-22 added prove reconstruction for injective functions; added SMT_Utils to collect frequently used functions
2010-11-22 haftmann 2010-11-22 generous timeout gives more breath in parallel run on less luxury machines
2010-11-22 bulwahn 2010-11-22 adding setup for exhaustive testing in example file
2010-11-22 bulwahn 2010-11-22 hiding enum
2010-11-22 bulwahn 2010-11-22 adapting example in Predicate_Compile_Examples
2010-11-22 bulwahn 2010-11-22 hiding the constants
2010-11-22 bulwahn 2010-11-22 improving function is_iterable in quickcheck
2010-11-22 bulwahn 2010-11-22 adding temporary options to the quickcheck examples
2010-11-22 bulwahn 2010-11-22 adapting the quickcheck examples
2010-11-22 bulwahn 2010-11-22 adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
2010-11-22 bulwahn 2010-11-22 adding code equations for EX1 on finite types