src/HOL/Tools/Transfer/transfer_bnf.ML
2 months ago wenzelm 2019-06-04 misc tuning and clarification, notably wrt. flow of context;
7 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
18 months ago wenzelm 2018-02-23 tuned signature -- eliminated clones;
2016-09-12 blanchet 2016-09-12 make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
2016-06-23 wenzelm 2016-06-23 tuned signature;
2016-05-27 wenzelm 2016-05-27 tuned proofs, to allow unfold_abs_def;
2016-04-17 wenzelm 2016-04-17 clarified signature;
2016-03-06 traytel 2016-03-06 less resetting of local theories
2016-03-05 wenzelm 2016-03-05 tuned signature;
2016-02-17 blanchet 2016-02-17 making 'pred_inject' a first-class BNF citizen
2016-02-17 blanchet 2016-02-17 refactoring
2016-02-17 traytel 2016-02-17 derive transfer rule for predicator
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2015-12-01 blanchet 2015-12-01 reverted inadvertently qfinished/pushed change r164eeb2ab675
2015-12-01 blanchet 2015-12-01 set "transfer_rule" attribute more generously
2015-10-07 blanchet 2015-10-07 disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-16 traytel 2015-07-16 {r,e,d,f}tac with proper context in BNF
2014-11-18 kuncar 2014-11-18 tuned; store pred_simps
2014-11-18 kuncar 2014-11-18 added pred_def, rel_eq_onp tuned
2015-04-28 blanchet 2015-04-28 allow sorts on dead variables in BNFs
2015-03-27 blanchet 2015-03-27 more graceful failure if some of the involved BNFs have no data
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;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-01-05 blanchet 2015-01-05 tuning
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-10-25 wenzelm 2014-10-25 made SML/NJ happy;
2014-10-20 kuncar 2014-10-20 register transfer rules from BNF and FP_Sugar
2014-10-20 kuncar 2014-10-20 refactored
2014-10-13 wenzelm 2014-10-13 Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-17 blanchet 2014-09-17 added missing 'restore' in 'transfer' plugin
2014-09-08 blanchet 2014-09-08 honour sorts in N2M
2014-09-08 blanchet 2014-09-08 made code work also in the presence of deads
2014-09-08 blanchet 2014-09-08 use right sort constraints
2014-09-05 blanchet 2014-09-05 pretend code generation is a ctr_sugar plugin
2014-09-05 blanchet 2014-09-05 named interpretations
2014-09-04 blanchet 2014-09-04 tuned size function generation
2014-09-03 blanchet 2014-09-03 introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
2014-08-11 traytel 2014-08-11 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
2014-06-27 blanchet 2014-06-27 compile
2014-04-23 kuncar 2014-04-23 predicator simplification rules: support also partially specialized types e.g. 'a * nat
2014-04-23 blanchet 2014-04-23 localize new size function generation code
2014-04-23 blanchet 2014-04-23 manual merge + added 'rel_distincts' field to record for symmetry
2014-04-11 kuncar 2014-04-11 observe also DEADID BNFs and associate the conjunction in rel_inject to the right
2014-04-10 kuncar 2014-04-10 setup for Transfer and Lifting from BNF; tuned thm names