2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-15 wenzelm 2010-05-15 tuned;
2010-05-15 wenzelm 2010-05-15 merged
2010-05-15 huffman 2010-05-15 add real_le_linear to list of legacy theorem names
2010-05-15 blanchet 2010-05-15 make SML/NJ happy
2010-05-15 wenzelm 2010-05-15 removed unused conversions;
2010-05-15 wenzelm 2010-05-15 tuned header; tuned white space;
2010-05-15 wenzelm 2010-05-15 moved normarith.ML where it is actually used; less inaccurate dependencies;
2010-05-15 wenzelm 2010-05-15 incorporated further conversions and conversionals, after some minor tuning;
2010-05-15 wenzelm 2010-05-15 eliminated redundant runtime checks;
2010-05-15 krauss 2010-05-15 normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
2010-05-15 wenzelm 2010-05-15 more precise dependencies for HOL-Word-SMT_Examples;
2010-05-15 wenzelm 2010-05-15 merged
2010-05-14 blanchet 2010-05-14 merge
2010-05-14 blanchet 2010-05-14 added Sledgehammer documentation to TOC
2010-05-14 blanchet 2010-05-14 added some Sledgehammer news
2010-05-14 blanchet 2010-05-14 document Nitpick changes
2010-05-14 blanchet 2010-05-14 merge
2010-05-14 blanchet 2010-05-14 added Sledgehammer manual; some material was recovered from the Isar material, the rest is new
2010-05-14 blanchet 2010-05-14 renamed Sledgehammer options
2010-05-14 blanchet 2010-05-14 renamed options
2010-05-14 blanchet 2010-05-14 remove support for crashing beta solver HaifaSat
2010-05-14 blanchet 2010-05-14 renamed two Sledgehammer options
2010-05-14 nipkow 2010-05-14 merged
2010-05-14 nipkow 2010-05-14 added listsum lemmas
2010-05-14 ballarin 2010-05-14 Revert mixin patch due to inacceptable performance drop.
2010-05-14 blanchet 2010-05-14 add "no_atp"s to Nitpick lemmas
2010-05-14 blanchet 2010-05-14 query _HOME environment variables at run-time, not at build-time
2010-05-14 blanchet 2010-05-14 move Refute dependency from Plain to Main
2010-05-14 blanchet 2010-05-14 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
2010-05-14 blanchet 2010-05-14 recognize new Kodkod error message syntax
2010-05-14 blanchet 2010-05-14 improve precision of set constructs in Nitpick
2010-05-14 blanchet 2010-05-14 produce more potential counterexamples for subset operator (cf. quantifiers)
2010-05-14 blanchet 2010-05-14 improved Sledgehammer proofs
2010-05-14 blanchet 2010-05-14 pass "full_type" argument to proof reconstruction
2010-05-14 blanchet 2010-05-14 made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code
2010-05-14 blanchet 2010-05-14 delect installed ATPs dynamically, _not_ at image built time
2010-05-13 ballarin 2010-05-13 Fix syntax; apparently constant apply was introduced in an earlier changeset.
2010-05-13 ballarin 2010-05-13 Merged.
2010-05-13 ballarin 2010-05-13 Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
2010-05-13 ballarin 2010-05-13 Remove improper use of mixin in class package.
2010-05-13 nipkow 2010-05-13 Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1
2010-05-12 huffman 2010-05-12 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
2010-05-13 boehmes 2010-05-13 more precise dependencies
2010-05-12 boehmes 2010-05-12 updated SMT certificates
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-05-12 boehmes 2010-05-12 integrated SMT into the HOL image
2010-05-12 boehmes 2010-05-12 replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
2010-05-12 boehmes 2010-05-12 use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
2010-05-12 boehmes 2010-05-12 split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)
2010-05-12 boehmes 2010-05-12 added tracing of reconstruction data
2010-05-12 boehmes 2010-05-12 added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
2010-05-12 boehmes 2010-05-12 deleted SMT translation files (to be replaced by a simplified version)
2010-05-12 boehmes 2010-05-12 move the addition of extra facts into a separate module
2010-05-12 boehmes 2010-05-12 normalize numerals: also rewrite Numeral0 into 0
2010-05-12 boehmes 2010-05-12 added missing rewrite rules for natural min and max
2010-05-12 boehmes 2010-05-12 rewrite bool case expressions as if expression
2010-05-12 boehmes 2010-05-12 simplified normalize_rule and moved it further down in the code
2010-05-12 boehmes 2010-05-12 merged addition of rules into one function