src/HOL/Transfer.thy
2014-09-04 blanchet 2014-09-04 tweaked setup for datatype realizer
2014-09-01 blanchet 2014-09-01 renamed BNF theories
2014-07-21 Andreas Lochbihler 2014-07-21 add parametricity lemmas
2014-06-27 blanchet 2014-06-27 merged two small theory files
2014-06-16 blanchet 2014-06-16 fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
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 qualify name
2014-04-11 kuncar 2014-04-11 bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
2014-04-10 kuncar 2014-04-10 setup for Transfer and Lifting from BNF; tuned thm names
2014-04-10 kuncar 2014-04-10 abstract Domainp in relator_domain rules => more natural statement of the rule
2014-04-10 kuncar 2014-04-10 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
2014-03-13 blanchet 2014-03-13 killed a few 'metis' calls
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-26 kuncar 2014-02-26 transfer domain rule for special case of functions - was missing
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-01-20 blanchet 2014-01-20 rationalized lemmas
2013-09-27 kuncar 2013-09-27 new parametricity rules and useful lemmas
2013-09-27 Andreas Lochbihler 2013-09-27 add lemmas
2013-09-26 Andreas Lochbihler 2013-09-26 add lemmas
2013-08-13 kuncar 2013-08-13 introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
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-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-03-16 kuncar 2013-03-16 fixing transfer tactic - unfold fully identity relation by using relator_eq
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
2012-10-24 huffman 2012-10-24 transfer package: more flexible handling of equality relations using is_equality predicate
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-05-16 kuncar 2012-05-16 generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
2012-05-15 huffman 2012-05-15 add transfer rules for nat_rec and funpow
2012-04-27 huffman 2012-04-27 implement transfer tactic with more scalable forward proof methods
2012-04-22 huffman 2012-04-22 tuned precedence order of transfer rules
2012-04-22 huffman 2012-04-22 new example theory for quotient/transfer
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 add transfer rule for nat_case
2012-04-20 huffman 2012-04-20 uniform naming scheme for transfer rules
2012-04-20 huffman 2012-04-20 rename 'correspondence' method to 'transfer_prover'
2012-04-20 huffman 2012-04-20 add secondary transfer rule for universal quantifiers on non-bi-total relations
2012-04-20 huffman 2012-04-20 add transfer rule for 'id'
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 add transfer rule for Let
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 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
2012-04-03 huffman 2012-04-03 new transfer proof method