src/HOL/Transfer.thy
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-12-05 kuncar 2014-12-05 Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
2015-02-11 Andreas Lochbihler 2015-02-11 more transfer rules
2015-02-11 Andreas Lochbihler 2015-02-11 add parametricity rule for Ex1
2015-02-11 Andreas Lochbihler 2015-02-11 add intro and elim rules for right_total
2015-01-05 blanchet 2015-01-05 tuning
2014-12-19 desharna 2014-12-19 Add plugin to generate transfer theorem for primrec and primcorec
2014-12-15 blanchet 2014-12-15 renamed theory file
2014-11-07 traytel 2014-11-07 more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-25 desharna 2014-09-25 generate 'corec_transfer' for codatatypes
2014-09-25 desharna 2014-09-25 generate 'ctor_rec_transfer' for datatypes
2014-09-19 traytel 2014-09-19 typo
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