src/HOL/Transfer.thy
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