2005-07-26 webertj 2005-07-26 comment modified
2005-07-26 webertj 2005-07-26 write_dimacs_sat_file writes outer parentheses again
2005-07-26 webertj 2005-07-26 replaced calls to PropLogic.defcnf by PropLogic.auxcnf
2005-07-26 webertj 2005-07-26 minor parameter changes
2005-07-25 webertj 2005-07-25 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
2005-07-25 avigad 2005-07-25 Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
2005-07-25 webertj 2005-07-25 defcnf modified to internally use a reference
2005-07-22 paulson 2005-07-22 dead code removal
2005-07-22 paulson 2005-07-22 reformatting and tidying
2005-07-22 paulson 2005-07-22 tidied up the tracing output
2005-07-22 paulson 2005-07-22 streamlined the tptp output
2005-07-22 paulson 2005-07-22 removed unused code
2005-07-22 berghofe 2005-07-22 Tuned comment.
2005-07-22 berghofe 2005-07-22 Rewrote function remove_suc, since it failed on some equations produced by recdef.
2005-07-21 webertj 2005-07-21 write_dimacs_sat_file now generates slightly smaller files
2005-07-20 paulson 2005-07-20 revised examples
2005-07-20 paulson 2005-07-20 code streamlining
2005-07-20 aspinall 2005-07-20 Ressurect seq attribute accidently removed
2005-07-20 kleing 2005-07-20 Sort search results in order of relevance, where relevance = a) better if 0 premises for intro or 1 premise for elim/dest rules b) better if substitution size wrt to current goal is smaller Only applies to intro, dest, elim, and simp (contributed by Rafal Kolanski, NICTA)
2005-07-19 wenzelm 2005-07-19 Inttab.defined;
2005-07-19 wenzelm 2005-07-19 some structured proofs on completeness;
2005-07-19 wenzelm 2005-07-19 more contribs;
2005-07-19 wenzelm 2005-07-19 tuned;
2005-07-19 wenzelm 2005-07-19 isatool fixheaders;
2005-07-19 wenzelm 2005-07-19 with_path;
2005-07-19 avigad 2005-07-19 added list of theorem changes to NEWS added real_of_int_abs to RealDef.thy
2005-07-19 wenzelm 2005-07-19 added defined;
2005-07-19 wenzelm 2005-07-19 simplified union;
2005-07-19 wenzelm 2005-07-19 tuned match, unify;
2005-07-19 wenzelm 2005-07-19 tuned instantiate (avoid subst_atomic, subst_atomic_types); Logic.incr_tvar;
2005-07-19 wenzelm 2005-07-19 tuned defs interface;
2005-07-19 wenzelm 2005-07-19 moved incr_tvar to logic.ML; added eq_var, eq_tvar, instantiate, instantiateT;
2005-07-19 wenzelm 2005-07-19 tuned norm_sort, mg_domain;
2005-07-19 wenzelm 2005-07-19 tuned instantiate interface; Logic.incr_tvar;
2005-07-19 wenzelm 2005-07-19 incr_tvar (from term.ML), incr_indexes: avoid garbage;
2005-07-19 wenzelm 2005-07-19 added has_duplicates; tuned qsort;
2005-07-19 wenzelm 2005-07-19 tuned interfaces declare, define, finalize, merge: canonical argument order, produce errors; tuned checkT';
2005-07-19 wenzelm 2005-07-19 Logic.incr_tvar;
2005-07-19 wenzelm 2005-07-19 retract accidental user commit; removed obsolete XSYMBOL_HOME; tuned;
2005-07-19 wenzelm 2005-07-19 tuned;
2005-07-19 obua 2005-07-19 proving bounds for real linear programs
2005-07-19 schirmer 2005-07-19 removed some garbage; fixed record_ex_sel_eq_simproc
2005-07-19 paulson 2005-07-19 textual tweak
2005-07-18 webertj 2005-07-18 Documentation updated
2005-07-18 haftmann 2005-07-18 reverted from fold_yield to fold_map
2005-07-15 wenzelm 2005-07-15 *** empty log message ***
2005-07-15 wenzelm 2005-07-15 tuned fold on terms and lists;
2005-07-15 wenzelm 2005-07-15 tuned assoc;
2005-07-15 wenzelm 2005-07-15 tuned fold on terms; tuned assoc;
2005-07-15 wenzelm 2005-07-15 tuned min_key, max_key;
2005-07-15 wenzelm 2005-07-15 replaced foldl_XXX by canonical fold_XXX; canonical arguments for add_term_varnames, add_tvarsT, add_tvars, add_vars, add_frees,
2005-07-15 wenzelm 2005-07-15 tuned;
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-07-15 wenzelm 2005-07-15 * Pure/library.ML: several combinators for linear functional transformations; * Pure/library.ML: canonical list combinators fold, fold_rev, and fold_yield; * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, fold_types;
2005-07-15 obua 2005-07-15 optimize no_types_needed, remove exception handler
2005-07-15 wenzelm 2005-07-15 tuned;
2005-07-14 dixon 2005-07-14 lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
2005-07-14 wenzelm 2005-07-14 * Improved 'oracle' command -- type-safe;
2005-07-14 wenzelm 2005-07-14 no open Logic;
2005-07-14 wenzelm 2005-07-14 removed itlist, rev_itlist -- use fold_rev, fold instead; improved end_itlist;