| Mon, 27 Nov 2006 17:35:50 +0100 |
webertj |
outermost universal quantifiers are stripped
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 20:34:21 +0100 |
wenzelm |
prefer antiquotations over LaTeX macros;
|
file |
diff |
annotate
|
| Thu, 26 Jan 2006 20:17:54 +0100 |
webertj |
smaller example to prevent timeout
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 15:16:06 +0100 |
webertj |
works with DPLL solver now
|
file |
diff |
annotate
|
| Tue, 26 Jul 2005 12:13:35 +0200 |
webertj |
minor parameter changes
|
file |
diff |
annotate
|
| Mon, 23 May 2005 17:17:06 +0200 |
webertj |
interpreters for lfp/gfp added
|
file |
diff |
annotate
|
| Mon, 18 Apr 2005 17:20:49 +0200 |
webertj |
support for recursion over mutually recursive IDTs
|
file |
diff |
annotate
|
| Wed, 23 Feb 2005 14:04:53 +0100 |
webertj |
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
|
file |
diff |
annotate
|
| Thu, 18 Nov 2004 18:46:09 +0100 |
webertj |
imports (new syntax for theory headers)
|
file |
diff |
annotate
|
| Thu, 26 Aug 2004 17:28:57 +0200 |
webertj |
comment modified
|
file |
diff |
annotate
|
| Wed, 26 May 2004 18:23:46 +0200 |
webertj |
mainly new/different datatype examples
|
file |
diff |
annotate
|
| Fri, 26 Mar 2004 19:58:43 +0100 |
webertj |
satsolver=dpll
|
file |
diff |
annotate
|
| Fri, 12 Mar 2004 10:47:59 +0100 |
webertj |
\<dots> replaced by ...
|
file |
diff |
annotate
|
| Thu, 11 Mar 2004 11:24:54 +0100 |
webertj |
Refute_Examples added/fixed
|
file |
diff |
annotate
|
| Wed, 10 Mar 2004 20:36:11 +0100 |
webertj |
Updated examples
|
file |
diff |
annotate
|
| Sat, 10 Jan 2004 13:35:10 +0100 |
webertj |
Adding 'refute' to HOL.
|
file |
diff |
annotate
|