src/HOL/Tools/refute.ML
Mon, 19 Sep 2005 23:45:59 +0200 webertj SAT solver interface modified to support proofs of unsatisfiability
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Thu, 08 Sep 2005 16:09:23 +0200 haftmann introduces some modern-style AList operations
Tue, 06 Sep 2005 16:59:48 +0200 wenzelm axclass: name space prefix is now "c_class" instead of just "c";
Mon, 05 Sep 2005 17:38:18 +0200 wenzelm curried_lookup/update;
Thu, 28 Jul 2005 15:19:51 +0200 wenzelm Sign.typ_match;
Fri, 17 Jun 2005 18:33:05 +0200 wenzelm accomodate change of TheoryDataFun;
Sat, 11 Jun 2005 22:15:51 +0200 wenzelm accomodate changed #classes;
Thu, 09 Jun 2005 12:03:18 +0200 wenzelm Theory.all_axioms_of;
Fri, 03 Jun 2005 14:35:33 +0200 webertj fixed a typo in the gfp interpreter
Wed, 25 May 2005 10:33:07 +0200 paulson SML/NJ compatibility
Mon, 23 May 2005 17:17:06 +0200 webertj interpreters for lfp/gfp added
Thu, 21 Apr 2005 18:57:18 +0200 berghofe Adapted to new interface of instantiation and unification / matching functions.
Wed, 20 Apr 2005 18:57:05 +0200 webertj call to Array.modifyi replaced
Tue, 19 Apr 2005 00:14:27 +0200 webertj compilation error fixed
Mon, 18 Apr 2005 17:20:49 +0200 webertj support for recursion over mutually recursive IDTs
Thu, 17 Mar 2005 01:40:18 +0100 webertj Bugfix related to the interpretation of IDT constructors
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 17:22:46 +0100 webertj interpreter for Finite_Set.Finites added
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
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
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Thu, 25 Nov 2004 20:33:35 +0100 webertj minor code refactoring (typ_of_dtyp, size_of_dtyp)
Thu, 25 Nov 2004 19:25:03 +0100 webertj exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
Thu, 25 Nov 2004 19:04:32 +0100 webertj comments edited
Wed, 17 Nov 2004 16:24:07 +0100 webertj minor changes (comments/code refactoring)
Sun, 14 Nov 2004 01:40:27 +0100 webertj DOCTYPE declaration added
Fri, 12 Nov 2004 20:55:04 +0100 webertj minor code refactoring
Mon, 09 Aug 2004 15:27:27 +0200 webertj warning for recursion over IDTs added
Mon, 21 Jun 2004 16:39:39 +0200 wenzelm immediate_output;
less more (0) -30 tip