testboard: File revisions

src/HOL/Tools/sat_funcs.ML

2009-07-27 ago	moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);	file \| diff \| annotate
2009-07-23 ago	more @{theory} antiquotations;	file \| diff \| annotate
2009-07-21 ago	proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;	file \| diff \| annotate
2009-07-15 ago	more antiquotations;	file \| diff \| annotate
2008-12-31 ago	moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);	file \| diff \| annotate
2008-06-10 ago	eliminated obsolete case_split_thm -- use case_split;	file \| diff \| annotate
2008-05-18 ago	moved global pretty/string_of functions from Sign to Syntax;	file \| diff \| annotate
2008-05-17 ago	cat_lines;	file \| diff \| annotate
2008-05-17 ago	structure Display: less pervasive operations;	file \| diff \| annotate
2007-07-05 ago	renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;	file \| diff \| annotate
2007-07-03 ago	Conjunction.intr/elim_balanced;	file \| diff \| annotate
2007-05-10 ago	moved conversions to structure Conv;	file \| diff \| annotate
2006-12-11 ago	ordered lists instead of tables for resolving hyps; speedup	file \| diff \| annotate
2006-12-10 ago	ML_Syntax.print_XXX;	file \| diff \| annotate
2006-11-29 ago	clauses sorted according to term order (significant speedup in some cases)	file \| diff \| annotate
2006-11-23 ago	renamed string_of_pair/list/option to ML_Syntax.str_of_pair/list/option;	file \| diff \| annotate
2006-11-09 ago	timing/tracing code removed	file \| diff \| annotate
2006-11-09 ago	interpreters for fst and snd added	file \| diff \| annotate
2006-09-06 ago	rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list	file \| diff \| annotate
2006-09-02 ago	tuned	file \| diff \| annotate
2006-08-30 ago	faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses	file \| diff \| annotate
2006-08-09 ago	tuned: string_of_list, string_of_pair	file \| diff \| annotate
2006-08-02 ago	proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust	file \| diff \| annotate
2006-07-20 ago	comments fixed, member function renamed	file \| diff \| annotate
2006-07-10 ago	minor optimization wrt. certifying terms	file \| diff \| annotate
2006-07-07 ago	"solver" reference added to make the SAT solver configurable	file \| diff \| annotate
2006-07-03 ago	comments fixed, minor optimization wrt. certifying terms	file \| diff \| annotate
2006-05-03 ago	pre_cnf_tac: beta-eta-normalization restricted to the current subgoal	file \| diff \| annotate
2006-05-02 ago	beta_eta_conversion added to pre_cnf_tac	file \| diff \| annotate
2006-03-10 ago	clauses now use (meta-)hyps instead of (meta-)implications; significant speedup	file \| diff \| annotate
2005-10-12 ago	counter added to SAT signature	file \| diff \| annotate
2005-10-12 ago	no proof reconstruction when quick_and_dirty is set	file \| diff \| annotate
2005-10-09 ago	Tactics sat and satx reimplemented, several improvements	file \| diff \| annotate
2005-09-28 ago	pre_sat_tac moved towards end of file	file \| diff \| annotate
2005-09-28 ago	comment fixed	file \| diff \| annotate
2005-09-24 ago	replay_proof optimized: now performs backwards proof search	file \| diff \| annotate
2005-09-24 ago	code reformatted and restructured, many minor modifications	file \| diff \| annotate
2005-09-23 ago	new sat tactic imports resolution proofs from zChaff	file \| diff \| annotate

testboard

RSS Atom