src/HOL/Tools/refute.ML
Wed, 26 May 2004 18:52:18 +0200 webertj adjusted for different signature of Type.typ_instance
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)
Fri, 16 Apr 2004 20:34:41 +0200 webertj exactly1true rewritten (much better when converting to CNF now)
Fri, 26 Mar 2004 14:53:17 +0100 webertj slightly different SAT solver interface
Thu, 11 Mar 2004 00:15:24 +0100 webertj SML/NJ compatibility fixes
Wed, 10 Mar 2004 22:33:48 +0100 webertj support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps
Mon, 12 Jan 2004 14:35:07 +0100 webertj Fixed compatibility issues with SML/NJ:
Sat, 10 Jan 2004 13:35:10 +0100 webertj Adding 'refute' to HOL.
less more (0) tip