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