src/Sequents/simpdata.ML
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-07-28 wenzelm 2015-07-28 more explicit context;
2015-03-07 wenzelm 2015-03-07 clarified Drule.gen_all: observe context more carefully;
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 match_tac etc.;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-01 wenzelm 2014-02-01 misc tuning and modernization;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-01-11 wenzelm 2012-01-11 more qualified names; more antiquotations;
2011-11-28 wenzelm 2011-11-28 avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
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-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-06-29 wenzelm 2011-06-29 tuned signature;
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2010-08-17 haftmann 2010-08-17 more antiquotations
2010-04-30 wenzelm 2010-04-30 proper context for rule_by_tactic;
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
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-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-07-23 wenzelm 2009-07-23 more @{theory} antiquotations;
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.;
2008-06-11 wenzelm 2008-06-11 converted ML proofs from simpdata.ML; tuned;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2007-05-09 wenzelm 2007-05-09 tuned ML setup;
2006-11-21 wenzelm 2006-11-21 removed legacy ML setup;
2006-11-20 wenzelm 2006-11-20 converted legacy ML scripts;
2005-10-18 wenzelm 2005-10-18 Simplifier.theory_context;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-09-18 wenzelm 2005-09-18 converted to Isar theory format;
2002-01-12 wenzelm 2002-01-12 renamed forall_elim_vars_safe to gen_all;
2002-01-11 wenzelm 2002-01-11 replace gen_all by forall_elim_vars_safe;
2000-08-29 wenzelm 2000-08-29 cong setup now part of Simplifier;
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-07-28 paulson 1999-07-28 congruence rule for |-, etc.
1999-07-27 paulson 1999-07-27 installation of simplifier and classical reasoner, better rules etc