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, 08 Dec 2010 08:33:02 +0100 | boehmes | be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts) | file | diff | annotate |
Tue, 07 Dec 2010 14:54:31 +0100 | boehmes | centralized handling of built-in types and constants for bitvectors | file | diff | annotate |
Tue, 07 Dec 2010 14:53:44 +0100 | boehmes | moved smt_word.ML into the directory of the Word library | file | diff | annotate |