2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-26 wenzelm 2015-07-26 updated to infer_instantiate; clarified context;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-06-02 wenzelm 2015-06-02 clarified context;
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 tuned signature -- prefer qualified names;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-04-09 wenzelm 2014-04-09 more standard names;
2014-04-09 wenzelm 2014-04-09 proper context for print_tac;
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-20 wenzelm 2014-03-20 more standard method_setup; enforce subgoal boundaries via SUBGOAL -- clean tactical failure if out-of-range;
2014-03-07 wenzelm 2014-03-07 more antiquotations;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-09-04 haftmann 2011-09-04 tuned
2011-09-03 huffman 2011-09-03 merged
2011-09-03 huffman 2011-09-03 modify nominal packages to better respect set/pred distinction
2011-09-03 haftmann 2011-09-03 assert Pure equations for theorem references; tuned
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-01-10 wenzelm 2011-01-10 standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
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-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-01-13 wenzelm 2010-01-13 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
2009-11-10 wenzelm 2009-11-10 eliminated some unused/obsolete Args.bang_facts;
2009-10-27 wenzelm 2009-10-27 Datatype.read_typ: standard argument order; eliminated some old folds;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-28 wenzelm 2009-09-28 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2008-09-22 urbanc 2008-09-22 made the perm_simp tactic to understand options such as (no_asm)
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 auxiliary dynamic_thm(s) for fact lookup; renamed local dynamic_thm(s) to goal_thm(s);
2008-01-28 berghofe 2008-01-28 Cleaned up simproc code.
2007-09-13 urbanc 2007-09-13 some cleaning up to do with contexts
2007-09-02 urbanc 2007-09-02 made theorem-references safe
2007-04-26 wenzelm 2007-04-26 eliminated unnamed infixes, tuned syntax;
2007-04-13 narboux 2007-04-13 debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
2007-04-07 urbanc 2007-04-07 tuned slightly the previous commit
2007-04-07 narboux 2007-04-07 perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
2007-04-04 narboux 2007-04-04 make fresh_guess fail if it does not solve the subgoal
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-04-03 narboux 2007-04-03 remove the lemma swap_fun which was not needed
2007-04-02 narboux 2007-04-02 rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
2007-03-28 urbanc 2007-03-28 the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
2007-03-06 urbanc 2007-03-06 major update of the nominal package; there is now an infrastructure for equivariance lemmas which eases definitions of nominal functions
2007-02-07 berghofe 2007-02-07 Adapted to changes in Finite_Set theory.