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
|