src/HOL/Lifting.thy
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-05-24 kuncar 2012-05-24 prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
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-16 kuncar 2012-05-16 infrastructure that makes possible to prove that a relation is reflexive
2012-05-04 huffman 2012-05-04 lifting package produces abs_eq_iff rules for total quotients
2012-04-26 kuncar 2012-04-26 use a quot_map theorem attribute instead of the complicated map attribute
2012-04-23 kuncar 2012-04-23 move MRSL to a separate file
2012-04-21 huffman 2012-04-21 move alternative definition lemmas into Lifting.thy; simplify proof of Quotient_compose
2012-04-21 huffman 2012-04-21 tuned proofs
2012-04-19 huffman 2012-04-19 generate abs_induct rules for quotient types
2012-04-18 kuncar 2012-04-18 Lifting: generate more thms & note them & tuned
2012-04-18 huffman 2012-04-18 move constant 'Respects' into Lifting.thy; add quantifier transfer rules for quotients
2012-04-18 huffman 2012-04-18 add lemma Quotient_abs_induct
2012-04-18 huffman 2012-04-18 more usage of context blocks
2012-04-18 huffman 2012-04-18 use context block
2012-04-18 huffman 2012-04-18 lifting_setup generates transfer rule for rep of typedefs
2012-04-18 huffman 2012-04-18 use context block to organize typedef lifting theorems
2012-04-17 kuncar 2012-04-17 tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
2012-04-16 kuncar 2012-04-16 leave Lifting prefix
2012-04-12 bulwahn 2012-04-12 merged
2012-04-04 griff 2012-04-04 manual merge
2012-04-05 huffman 2012-04-05 add transfer lemmas for quotients
2012-04-04 huffman 2012-04-04 merged
2012-04-04 huffman 2012-04-04 add lemmas for generating transfer rules for typedefs
2012-04-04 kuncar 2012-04-04 support non-open typedefs; define cr_rel in terms of a rep function for typedefs
2012-04-04 huffman 2012-04-04 update keywords file
2012-04-04 huffman 2012-04-04 lift_definition command generates transfer rule
2012-04-03 huffman 2012-04-03 new transfer proof method
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit