src/HOL/Quotient.thy
2010-08-25 Cezary Kaliszyk 2010-08-25 Quotient Package / lemma for regularization of bex1_rel for equivalence relations
2010-08-11 Christian Urban 2010-08-11 deleted duplicate lemma
2010-07-28 wenzelm 2010-07-28 use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);
2010-06-29 Christian Urban 2010-06-29 separated the lifting and descending procedures in the quotient package
2010-06-28 Cezary Kaliszyk 2010-06-28 Quotient package reverse lifting
2010-06-23 Cezary Kaliszyk 2010-06-23 Quotient package now uses Partial Equivalence instead place of equivalence
2010-05-21 Cezary Kaliszyk 2010-05-21 Let rsp and prs in fun_rel/fun_map format
2010-04-22 Cezary Kaliszyk 2010-04-22 fun_rel introduction and list_rel elimination for quotient package
2010-04-20 Cezary Kaliszyk 2010-04-20 respectfullness and preservation of function composition
2010-04-13 Cezary Kaliszyk 2010-04-13 add If respectfullness and preservation to Quotient package database
2010-04-12 Cezary Kaliszyk 2010-04-12 Changed the type of Quot_True, so that it is an HOL constant.
2010-03-17 blanchet 2010-03-17 renamed "ATP_Linkup" theory to "Sledgehammer"
2010-02-22 huffman 2010-02-22 proper header and subsection headings
2010-02-19 Cezary Kaliszyk 2010-02-19 quote the constant and theorem name with @{text}
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package.