isabelle: File revisions

src/HOL/Tools/refute.ML

2006-07-11	wenzelm	2006-07-11	removed obsolete mem_term;	file \| diff \| annotate
2006-05-16	wenzelm	2006-05-16	more abstract interface to classes/arities;	file \| diff \| annotate
2006-04-06	haftmann	2006-04-06	cleanup in datatype package	file \| diff \| annotate
2006-03-17	haftmann	2006-03-17	renamed op < <= to Orderings.less(_eq)	file \| diff \| annotate
2006-03-10	haftmann	2006-03-10	*renamed HOL + - etc. to HOL.plus HOL.minus HOL.times etc.**	file \| diff \| annotate
2006-02-06	wenzelm	2006-02-06	Logic.const_of_class/class_of_const;	file \| diff \| annotate
2006-01-23	webertj	2006-01-23	TimeLimit replaced by interrupt_timeout	file \| diff \| annotate
2006-01-19	wenzelm	2006-01-19	setup: theory -> theory;	file \| diff \| annotate
2006-01-14	wenzelm	2006-01-14	sane ERROR handling;	file \| diff \| annotate
2005-09-19	webertj	2005-09-19	SAT solver interface modified to support proofs of unsatisfiability	file \| diff \| annotate
2005-09-15	wenzelm	2005-09-15	TableFun/Symtab: curried lookup and update;	file \| diff \| annotate
2005-09-08	haftmann	2005-09-08	introduces some modern-style AList operations	file \| diff \| annotate
2005-09-06	wenzelm	2005-09-06	axclass: name space prefix is now "c_class" instead of just "c";	file \| diff \| annotate
2005-09-05	wenzelm	2005-09-05	curried_lookup/update;	file \| diff \| annotate
2005-07-28	wenzelm	2005-07-28	Sign.typ_match;	file \| diff \| annotate
2005-06-17	wenzelm	2005-06-17	accomodate change of TheoryDataFun;	file \| diff \| annotate
2005-06-11	wenzelm	2005-06-11	accomodate changed #classes;	file \| diff \| annotate
2005-06-09	wenzelm	2005-06-09	Theory.all_axioms_of;	file \| diff \| annotate
2005-06-03	webertj	2005-06-03	fixed a typo in the gfp interpreter	file \| diff \| annotate
2005-05-25	paulson	2005-05-25	SML/NJ compatibility	file \| diff \| annotate
2005-05-23	webertj	2005-05-23	interpreters for lfp/gfp added	file \| diff \| annotate
2005-04-21	berghofe	2005-04-21	Adapted to new interface of instantiation and unification / matching functions.	file \| diff \| annotate
2005-04-20	webertj	2005-04-20	call to Array.modifyi replaced	file \| diff \| annotate
2005-04-19	webertj	2005-04-19	compilation error fixed	file \| diff \| annotate
2005-04-18	webertj	2005-04-18	support for recursion over mutually recursive IDTs	file \| diff \| annotate
2005-03-17	webertj	2005-03-17	Bugfix related to the interpretation of IDT constructors	file \| diff \| annotate
2005-03-04	skalberg	2005-03-04	Removed practically all references to Library.foldr.	file \| diff \| annotate
2005-03-03	webertj	2005-03-03	interpreter for Finite_Set.Finites added	file \| diff \| annotate
2005-03-03	skalberg	2005-03-03	Move towards standard functions.	file \| diff \| annotate
2005-02-23	webertj	2005-02-23	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
2005-02-13	skalberg	2005-02-13	Deleted Library.option type.	file \| diff \| annotate
2004-11-25	webertj	2004-11-25	minor code refactoring (typ_of_dtyp, size_of_dtyp)	file \| diff \| annotate
2004-11-25	webertj	2004-11-25	exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)	file \| diff \| annotate
2004-11-25	webertj	2004-11-25	comments edited	file \| diff \| annotate
2004-11-17	webertj	2004-11-17	minor changes (comments/code refactoring)	file \| diff \| annotate
2004-11-14	webertj	2004-11-14	DOCTYPE declaration added	file \| diff \| annotate
2004-11-12	webertj	2004-11-12	minor code refactoring	file \| diff \| annotate
2004-08-09	webertj	2004-08-09	warning for recursion over IDTs added	file \| diff \| annotate
2004-06-21	wenzelm	2004-06-21	immediate_output;	file \| diff \| annotate
2004-06-17	webertj	2004-06-17	new SAT solver interface	file \| diff \| annotate
2004-05-29	wenzelm	2004-05-29	Output.output;	file \| diff \| annotate
2004-05-26	webertj	2004-05-26	adjusted for different signature of Type.typ_instance	file \| diff \| annotate
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)	file \| diff \| annotate
2004-04-16	webertj	2004-04-16	exactly1true rewritten (much better when converting to CNF now)	file \| diff \| annotate
2004-03-26	webertj	2004-03-26	slightly different SAT solver interface	file \| diff \| annotate
2004-03-11	webertj	2004-03-11	SML/NJ compatibility fixes	file \| diff \| annotate
2004-03-10	webertj	2004-03-10	support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps	file \| diff \| annotate
2004-01-12	webertj	2004-01-12	*Fixed compatibility issues with SML/NJ: - replaced '(op )' by 'op' - replaced 'LargeInt' by 'Int'*	file \| diff \| annotate
2004-01-10	webertj	2004-01-10	Adding 'refute' to HOL.	file \| diff \| annotate

isabelle

RSS Atom