src/HOL/Tools/refute.ML
2004-11-17 webertj 2004-11-17 minor changes (comments/code refactoring)
2004-11-14 webertj 2004-11-14 DOCTYPE declaration added
2004-11-12 webertj 2004-11-12 minor code refactoring
2004-08-09 webertj 2004-08-09 warning for recursion over IDTs added
2004-06-21 wenzelm 2004-06-21 immediate_output;
2004-06-17 webertj 2004-06-17 new SAT solver interface
2004-05-29 wenzelm 2004-05-29 Output.output;
2004-05-26 webertj 2004-05-26 adjusted for different signature of Type.typ_instance
2004-05-26 webertj 2004-05-26 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)
2004-04-16 webertj 2004-04-16 exactly1true rewritten (much better when converting to CNF now)
2004-03-26 webertj 2004-03-26 slightly different SAT solver interface
2004-03-11 webertj 2004-03-11 SML/NJ compatibility fixes
2004-03-10 webertj 2004-03-10 support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps
2004-01-12 webertj 2004-01-12 Fixed compatibility issues with SML/NJ: - replaced '(op *)' by 'op*' - replaced 'LargeInt' by 'Int'
2004-01-10 webertj 2004-01-10 Adding 'refute' to HOL.