src/HOL/Tools/transfer.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-02-25 kuncar 2014-02-25 rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
2014-02-18 kuncar 2014-02-18 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
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-09-16 kuncar 2013-09-16 public access to the raw transfer rules - for restoring transferring
2013-08-22 kuncar 2013-08-22 delete corresponding compound lhs and rhs when a transfer rule is deleted; tuned
2013-08-22 kuncar 2013-08-22 publish a private function
2013-08-21 kuncar 2013-08-21 double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
2013-08-16 wenzelm 2013-08-16 standardized aliases;
2013-08-07 kuncar 2013-08-07 contract equalities in transfer and transfer domain rules when they are registered
2013-08-07 kuncar 2013-08-07 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
2013-06-10 huffman 2013-06-10 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
2013-06-08 huffman 2013-06-08 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
2013-05-15 kuncar 2013-05-15 abstract equalities only in a correspondence relation in a transfer domain rule
2013-05-13 kuncar 2013-05-13 better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
2013-05-13 kuncar 2013-05-13 try to detect assumptions of transfer rules that are in a shape of a transfer rule
2013-05-13 kuncar 2013-05-13 publish a private function
2013-03-16 kuncar 2013-03-16 fixing transfer tactic - unfold fully identity relation by using relator_eq
2013-03-08 kuncar 2013-03-08 lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
2013-02-28 wenzelm 2013-02-28 just one HOLogic.Trueprop_conv, with regular exception CTERM; tuned;
2012-10-24 huffman 2012-10-24 transfer package: error message if preprocessing goal to object-logic formula fails
2012-10-24 huffman 2012-10-24 transfer package: add test to prevent trying to make cterms from open terms
2012-10-24 huffman 2012-10-24 transfer package: more flexible handling of equality relations using is_equality predicate
2012-09-27 kuncar 2012-09-27 new get function for non-symmetric relator_eq & tuned
2012-06-02 huffman 2012-06-02 transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
2012-06-01 huffman 2012-06-01 transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
2012-06-01 huffman 2012-06-01 unify theory-data structures for transfer package
2012-04-27 huffman 2012-04-27 allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing
2012-04-27 huffman 2012-04-27 implement transfer tactic with more scalable forward proof methods
2012-04-21 huffman 2012-04-21 enable variant of transfer method that proves an implication instead of an equivalence
2012-04-20 huffman 2012-04-20 rename 'correspondence' method to 'transfer_prover'
2012-04-20 huffman 2012-04-20 make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
2012-04-19 huffman 2012-04-19 use simpler method for preserving bound variable names in transfer tactic
2012-04-18 huffman 2012-04-18 add option to transfer method for specifying variables not to generalize over
2012-04-17 huffman 2012-04-17 make transfer method more deterministic by using SOLVED' on some subgoals
2012-04-17 huffman 2012-04-17 add theory data for relator identity rules; preprocess transfer rules generated by lift_definition using relator rules
2012-04-04 huffman 2012-04-04 transfer method generalizes over free variables in goal
2012-04-04 huffman 2012-04-04 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
2012-04-04 huffman 2012-04-04 add type annotations to make SML happy (cf. ec6187036495)
2012-04-03 huffman 2012-04-03 new transfer proof method
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
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-11-09 wenzelm 2011-11-09 misc tuning;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-07-08 haftmann 2010-07-08 tuned titles
2010-03-18 haftmann 2010-03-18 meaningful transfer certificate
2010-03-11 haftmann 2010-03-11 made smlnj happy
2010-03-09 haftmann 2010-03-09 clarified transfer code proper; more natural declaration of return rules
2010-03-09 haftmann 2010-03-09 data administration using canonical functorial operations
2010-03-09 haftmann 2010-03-09 tuned data structures; using AList.map_default
2010-03-09 haftmann 2010-03-09 consistent field names; tuned interface
2010-03-08 haftmann 2010-03-08 proper ML interface; further polishing
2010-03-08 haftmann 2010-03-08 code simplification and tuning
2010-03-08 haftmann 2010-03-08 transfer: avoid camel case, more standard coding conventions, misc tuning
2010-03-07 haftmann 2010-03-07 dropped dead code; adhere more closely to standard coding conventions
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-29 haftmann 2009-10-29 join entries properly on theory merge
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation