isabelle: Shortlog

Mercurial Mercurial > repos > isabelle / shortlog

2010-05-14	blanchet	add "no_atp"s to Nitpick lemmas	changeset \| files
2010-05-14	blanchet	query _HOME environment variables at run-time, not at build-time	changeset \| files
2010-05-14	blanchet	move Refute dependency from Plain to Main	changeset \| files
2010-05-14	blanchet	move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong	changeset \| files
2010-05-14	blanchet	recognize new Kodkod error message syntax	changeset \| files
2010-05-14	blanchet	improve precision of set constructs in Nitpick	changeset \| files
2010-05-14	blanchet	produce more potential counterexamples for subset operator (cf. quantifiers)	changeset \| files
2010-05-14	blanchet	improved Sledgehammer proofs	changeset \| files
2010-05-14	blanchet	pass "full_type" argument to proof reconstruction	changeset \| files
2010-05-14	blanchet	made Sledgehammer's full-typed proof reconstruction work for the first time;	changeset \| files
2010-05-14	blanchet	delect installed ATPs dynamically, _not_ at image built time	changeset \| files
2010-05-13	ballarin	Fix syntax; apparently constant apply was introduced in an earlier changeset.	changeset \| files
2010-05-13	ballarin	Merged.	changeset \| files
2010-05-13	ballarin	Add mixin to base morphism, required by class package; cf ab324ffd6f3d.	changeset \| files
2010-05-13	ballarin	Remove improper use of mixin in class package.	changeset \| files
2010-05-13	nipkow	Multiset: renamed, added and tuned lemmas;	changeset \| files
2010-05-13	huffman	use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document	changeset \| files
2010-05-12	boehmes	more precise dependencies	changeset \| files
2010-05-12	boehmes	updated SMT certificates	changeset \| files
2010-05-12	boehmes	layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable	changeset \| files
2010-05-12	boehmes	integrated SMT into the HOL image	changeset \| files
2010-05-12	boehmes	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	changeset \| files
2010-05-12	boehmes	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)	changeset \| files
2010-05-12	boehmes	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)	changeset \| files
2010-05-12	boehmes	added tracing of reconstruction data	changeset \| files
2010-05-12	boehmes	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	changeset \| files
2010-05-12	boehmes	deleted SMT translation files (to be replaced by a simplified version)	changeset \| files
2010-05-12	boehmes	move the addition of extra facts into a separate module	changeset \| files

(0) -30000 -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle

RSS Atom