| Thu, 29 Oct 2020 09:59:40 +0000 |
haftmann |
removed dependency
|
file |
diff |
annotate
|
| Mon, 26 Oct 2020 11:28:43 +0000 |
haftmann |
factored out theory Traditional_Syntax
|
file |
diff |
annotate
|
| Sat, 17 Oct 2020 19:10:40 +0200 |
haftmann |
early and more complete setup of tools
|
file |
diff |
annotate
|
| Sat, 09 May 2020 17:20:04 +0000 |
haftmann |
modernized notation for bit operations
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 18:30:23 +0200 |
blanchet |
towards support for HO SMT-LIB
|
file |
diff |
annotate
|
| Mon, 20 Mar 2017 21:44:41 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
| base
|
| Tue, 17 Apr 2012 16:21:47 +1000 |
Thomas Sewell |
New tactic "word_bitwise" expands word equalities/inequalities into logic.
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 15:31:49 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 09:41:48 +0100 |
boehmes |
avoid ML structure aliases (especially single-letter abbreviations)
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 18:54:29 +0100 |
boehmes |
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
|
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, 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
|