| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
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
|
| Tue, 30 Nov 2010 20:52:49 +0100 |
haftmann |
code preprocessor setup for numerals on word type;
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 16:05:25 +0200 |
haftmann |
constant `contents` renamed to `the_elem`
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 14:55:10 +0200 |
haftmann |
moved spurious auxiliary lemma here
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Fri, 09 Jul 2010 08:11:10 +0200 |
haftmann |
nicer xsymbol syntax for fcomp and scomp
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 13:32:14 +0200 |
haftmann |
avoid bitstrings in generated code
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 17:12:38 +0200 |
haftmann |
one unified Word theory
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:32 +0100 |
haftmann |
tuned spelling
|
file |
diff |
annotate
|
| Mon, 26 Jan 2009 22:14:16 +0100 |
haftmann |
entry point for Word library now named Word
|
file |
diff |
annotate
| base
|