| 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
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Thu, 25 Nov 2004 20:33:35 +0100 |
webertj |
minor code refactoring (typ_of_dtyp, size_of_dtyp)
|
file |
diff |
annotate
|
| Thu, 25 Nov 2004 19:25:03 +0100 |
webertj |
exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
|
file |
diff |
annotate
|
| Thu, 25 Nov 2004 19:04:32 +0100 |
webertj |
comments edited
|
file |
diff |
annotate
|
| Wed, 17 Nov 2004 16:24:07 +0100 |
webertj |
minor changes (comments/code refactoring)
|
file |
diff |
annotate
|
| Sun, 14 Nov 2004 01:40:27 +0100 |
webertj |
DOCTYPE declaration added
|
file |
diff |
annotate
|
| Fri, 12 Nov 2004 20:55:04 +0100 |
webertj |
minor code refactoring
|
file |
diff |
annotate
|
| Mon, 09 Aug 2004 15:27:27 +0200 |
webertj |
warning for recursion over IDTs added
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 16:39:39 +0200 |
wenzelm |
immediate_output;
|
file |
diff |
annotate
|
| Thu, 17 Jun 2004 22:01:23 +0200 |
webertj |
new SAT solver interface
|
file |
diff |
annotate
|
| Sat, 29 May 2004 14:57:39 +0200 |
wenzelm |
Output.output;
|
file |
diff |
annotate
|
| Wed, 26 May 2004 18:52:18 +0200 |
webertj |
adjusted for different signature of Type.typ_instance
|
file |
diff |
annotate
|
| Wed, 26 May 2004 18:03:52 +0200 |
webertj |
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 20:34:41 +0200 |
webertj |
exactly1true rewritten (much better when converting to CNF now)
|
file |
diff |
annotate
|