isabelle: File revisions

Mercurial Mercurial > repos > isabelle / file revisions

summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip

src/HOL/Tools/SMT/smt_utils.ML

Mon, 20 Dec 2010 08:45:27 +0100	boehmes	derived SMT solver classes override inherited properties (properties of derived classes have a higher priority than properties of base classes)	file \| diff \| annotate
Sun, 19 Dec 2010 17:55:56 +0100	boehmes	only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);	file \| diff \| annotate
Wed, 15 Dec 2010 16:29:56 +0100	boehmes	the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils	file \| diff \| annotate
Wed, 15 Dec 2010 10:12:44 +0100	boehmes	re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);	file \| diff \| annotate
Wed, 15 Dec 2010 08:39:24 +0100	boehmes	re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);	file \| diff \| annotate
Wed, 15 Dec 2010 08:39:24 +0100	boehmes	moved SMT classes and dictionary functions to SMT_Utils	file \| diff \| annotate
Wed, 15 Dec 2010 08:39:24 +0100	boehmes	tuned	file \| diff \| annotate
Wed, 01 Dec 2010 13:09:08 +0100	wenzelm	just one Term.dest_funT;	file \| diff \| annotate
Mon, 22 Nov 2010 15:45:43 +0100	boehmes	share and use more utility functions;	file \| diff \| annotate
Mon, 22 Nov 2010 15:45:42 +0100	boehmes	added prove reconstruction for injective functions;	file \| diff \| annotate

less more (0) tip

isabelle