2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems; modernized setup;
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-05-30 wenzelm 2013-05-30 standardized aliases;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-02-14 wenzelm 2012-02-14 simplified use of tacticals;
2011-12-07 Christian Urban 2011-12-07 added a specific tactic and method that deal with partial equivalence relations
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-05 Christian Urban 2011-11-05 more use of global operations (see 98ec8b51af9c)
2011-10-27 wenzelm 2011-10-27 simplified/standardized signatures;
2011-08-19 Cezary Kaliszyk 2011-08-19 Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.
2011-07-20 Cezary Kaliszyk 2011-07-20 Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-07 wenzelm 2011-01-07 do not open ML structures;
2011-01-07 wenzelm 2011-01-07 more precise parentheses and indentation; eliminated trailing whitespace;
2011-01-07 wenzelm 2011-01-07 comments;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-01 wenzelm 2010-12-01 just one Term.dest_funT;
2010-11-18 haftmann 2010-11-18 map_fun combinator in theory Fun
2010-11-09 haftmann 2010-11-09 slightly changed fun_map_def
2010-08-30 haftmann 2010-08-30 merged
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-30 Cezary Kaliszyk 2010-08-30 Quotient Package: dont unfold mem_def, use rsp and prs instead
2010-08-28 Christian Urban 2010-08-28 quotient package: added a list of pre-simplification rules for Ball, Bex and mem
2010-08-28 Christian Urban 2010-08-28 quotient package: lemmas to be lifted and descended can be pre-simplified
2010-08-25 wenzelm 2010-08-25 merged
2010-08-25 Christian Urban 2010-08-25 tuned code
2010-08-25 Christian Urban 2010-08-25 quotient package: deal correctly with frees in lifted theorems
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-24 Christian Urban 2010-08-24 use matching of types than just equality - this is needed in nominal to cope with type variables
2010-08-22 Christian Urban 2010-08-22 use a smaller simpset in order to not solve refl-instances
2010-08-22 Christian Urban 2010-08-22 allow for pre-simplification of lifted theorems
2010-08-22 Christian Urban 2010-08-22 changed to a more convenient argument order
2010-08-11 Christian Urban 2010-08-11 deleted duplicate lemma
2010-07-08 haftmann 2010-07-08 tuned titles
2010-06-29 Christian Urban 2010-06-29 separated the lifting and descending procedures in the quotient package
2010-06-28 Christian Urban 2010-06-28 separation of translations in derive_qtrm / derive_rtrm (similarly for types)
2010-06-28 Cezary Kaliszyk 2010-06-28 Quotient package reverse lifting
2010-06-28 Cezary Kaliszyk 2010-06-28 Add reverse lifting flag to automated theorem derivation
2010-06-26 Christian Urban 2010-06-26 streamlined the generation of quotient theorems out of raw theorems
2010-06-23 Cezary Kaliszyk 2010-06-23 Quotient package now uses Partial Equivalence instead place of equivalence
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-15 wenzelm 2010-05-15 incorporated further conversions and conversionals, after some minor tuning;
2010-05-12 Cezary Kaliszyk 2010-05-12 Remove RANGE_WARN
2010-05-03 wenzelm 2010-05-03 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-04-20 Cezary Kaliszyk 2010-04-20 eta-normalize the goal since the original theorem is atomized
2010-03-27 Cezary Kaliszyk 2010-03-27 Automated lifting can be restricted to specific quotient types
2010-03-19 Cezary Kaliszyk 2010-03-19 Check that argument is not a 'Bound' before calling fastype_of.
2010-03-14 wenzelm 2010-03-14 tuned comment;