2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-25 wenzelm 2010-08-25 structure Thm: less pervasive names;
2010-08-20 haftmann 2010-08-20 merged
2010-08-20 haftmann 2010-08-20 split and enriched theory SetsAndFunctions
2010-08-20 blanchet 2010-08-20 merged
2010-08-20 blanchet 2010-08-20 beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly); another consequence of the transition to FOF
2010-08-19 blanchet 2010-08-19 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
2010-08-19 haftmann 2010-08-19 more antiquotations
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-29 blanchet 2010-07-29 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
2010-07-29 blanchet 2010-07-29 perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
2010-07-21 blanchet 2010-07-21 renamings + only need second component of name pool to reconstruct proofs
2010-07-12 wenzelm 2010-07-12 moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
2010-06-24 blanchet 2010-06-24 cosmetics
2010-06-14 blanchet 2010-06-14 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-11 blanchet 2010-06-11 beta-eta-contract, to respect "first_order_match"'s specification; Sledgehammer's Skolem cache sometimes failed without the contraction
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-04-30 wenzelm 2010-04-30 renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2010-03-28 wenzelm 2010-03-28 static defaults for configuration options;
2010-03-22 blanchet 2010-03-22 merged
2010-03-22 blanchet 2010-03-22 start work on direct proof reconstruction for Sledgehammer
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-11-21 wenzelm 2009-11-21 explicitly mark some legacy freeze operations;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-27 wenzelm 2009-10-27 critical comments;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-16 wenzelm 2009-10-16 local channels for tracing/debugging;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-29 wenzelm 2009-07-29 Meson.first_order_resolve: avoid handle _; proper context for various Meson and Metis rules and tactics unified meson_tac/meson_claset_tac;
2009-07-27 wenzelm 2009-07-27 moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-06-04 haftmann 2009-06-04 dropped legacy ML bindings; tuned
2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-29 paulson 2009-01-29 Minor reorganisation of the Skolemization code
2008-12-31 wenzelm 2008-12-31 use exists_subterm directly;
2008-09-29 wenzelm 2008-09-29 handle _ should be avoided (spurious Interrupt will spoil the game);
2008-09-09 paulson 2008-09-09 more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-16 wenzelm 2008-06-16 RuleInsts.read_instantiate;
2008-06-11 wenzelm 2008-06-11 Drule.read_instantiate;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-07 paulson 2008-04-07 * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2008-02-13 paulson 2008-02-13 make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
2007-12-19 paulson 2007-12-19 Replaced refs by config params; finer critical section in mets method
2007-12-18 paulson 2007-12-18 Skolemization now catches exception THM, which may be raised if unification fails.
2007-10-09 paulson 2007-10-09 context-based treatment of generalization; also handling TFrees in axiom clauses
2007-10-04 paulson 2007-10-04 combinator translation
2007-09-27 paulson 2007-09-27 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions