| Mon, 06 Feb 2006 20:58:59 +0100 |
wenzelm |
Logic.const_of_class/class_of_const;
|
file |
diff |
annotate
|
| Mon, 23 Jan 2006 17:29:52 +0100 |
webertj |
TimeLimit replaced by interrupt_timeout
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 23:45:59 +0200 |
webertj |
SAT solver interface modified to support proofs of unsatisfiability
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Thu, 08 Sep 2005 16:09:23 +0200 |
haftmann |
introduces some modern-style AList operations
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 16:59:48 +0200 |
wenzelm |
axclass: name space prefix is now "c_class" instead of just "c";
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 17:38:18 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:19:51 +0200 |
wenzelm |
Sign.typ_match;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:05 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2005 22:15:51 +0200 |
wenzelm |
accomodate changed #classes;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2005 12:03:18 +0200 |
wenzelm |
Theory.all_axioms_of;
|
file |
diff |
annotate
|
| Fri, 03 Jun 2005 14:35:33 +0200 |
webertj |
fixed a typo in the gfp interpreter
|
file |
diff |
annotate
|
| Wed, 25 May 2005 10:33:07 +0200 |
paulson |
SML/NJ compatibility
|
file |
diff |
annotate
|
| Mon, 23 May 2005 17:17:06 +0200 |
webertj |
interpreters for lfp/gfp added
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 18:57:18 +0200 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
file |
diff |
annotate
|
| Wed, 20 Apr 2005 18:57:05 +0200 |
webertj |
call to Array.modifyi replaced
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 00:14:27 +0200 |
webertj |
compilation error fixed
|
file |
diff |
annotate
|
| Mon, 18 Apr 2005 17:20:49 +0200 |
webertj |
support for recursion over mutually recursive IDTs
|
file |
diff |
annotate
|
| Thu, 17 Mar 2005 01:40:18 +0100 |
webertj |
Bugfix related to the interpretation of IDT constructors
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 17:22:46 +0100 |
webertj |
interpreter for Finite_Set.Finites added
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
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
|
| 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
|
| Fri, 26 Mar 2004 14:53:17 +0100 |
webertj |
slightly different SAT solver interface
|
file |
diff |
annotate
|
| Thu, 11 Mar 2004 00:15:24 +0100 |
webertj |
SML/NJ compatibility fixes
|
file |
diff |
annotate
|
| Wed, 10 Mar 2004 22:33:48 +0100 |
webertj |
support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 14:35:07 +0100 |
webertj |
Fixed compatibility issues with SML/NJ:
|
file |
diff |
annotate
|
| Sat, 10 Jan 2004 13:35:10 +0100 |
webertj |
Adding 'refute' to HOL.
|
file |
diff |
annotate
|