src/Tools/case_product.ML
15 months ago wenzelm 2018-01-28 clarified take/drop/chop prefix/suffix;
17 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
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-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-29 wenzelm 2014-10-29 modernized setup;
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-07-27 wenzelm 2013-07-27 standardized aliases;
2012-08-23 wenzelm 2012-08-23 prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2011-08-01 nipkow 2011-08-01 infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-03 wenzelm 2011-03-03 observe standard header format;
2010-12-08 noschinl 2010-12-08 introduce attribute case_prod for combining case rules * * * [PATCH 1/9] Make tac independent of consumes From 1a53ef4c070f924ff8e69529b0c1b13fa2844722 Mon Sep 17 00:00:00 2001 --- case_product.ML | 11 ++++++----- 1 files changed, 6 insertions(+), 5 deletions(-) * * * [PATCH 2/9] Replace MRS by OF From da55d08ae287bfdc18dec554067b45a3e298c243 Mon Sep 17 00:00:00 2001 --- case_product.ML | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) * * * [PATCH 3/9] Clean up tactic From d26d50caaa3526c8c0625d7395467c6914f1a8d9 Mon Sep 17 00:00:00 2001 --- case_product.ML | 13 +++++-------- 1 files changed, 5 insertions(+), 8 deletions(-) * * * [PATCH 4/9] Move out get_consumes a bit more From 6ed5415f29cc43cea30c216edb1e74ec6c0f6c33 Mon Sep 17 00:00:00 2001 --- case_product.ML | 4 +++- 1 files changed, 3 insertions(+), 1 deletions(-) * * * [PATCH 5/9] Clean up tactic From d301cfe6377e9f7db74b190fb085e0e66eeadfb5 Mon Sep 17 00:00:00 2001 --- case_product.ML | 3 +-- 1 files changed, 1 insertions(+), 2 deletions(-) * * * [PATCH 6/9] Cleanup build_concl_prems From c30889e131e74a92caac5b1e6d3d816890406ca7 Mon Sep 17 00:00:00 2001 --- case_product.ML | 18 ++++++++---------- 1 files changed, 8 insertions(+), 10 deletions(-) * * * [PATCH 7/9] Split logic & annotation a bit From e065606118308c96e013fad72ab9ad89b5a4b945 Mon Sep 17 00:00:00 2001 --- case_product.ML | 26 ++++++++++++++++++-------- 1 files changed, 18 insertions(+), 8 deletions(-) * * * [PATCH 8/9] Remove dependency on consumes attribute From e2a4de044481586d6127bbabd0ef48d0e3ab57c0 Mon Sep 17 00:00:00 2001 --- case_product.ML | 46 ++++++++++++++++++++++------------------------ 1 files changed, 22 insertions(+), 24 deletions(-) * * * [PATCH 9/9] whitespace From 59f5036bd8f825da4a362970292a34ec06c0f1a2 Mon Sep 17 00:00:00 2001 --- case_product.ML | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-)