src/HOL/Quotient.thy
2011-08-16 haftmann 2011-08-16 avoid Collect_def in proof
2011-08-16 Cezary Kaliszyk 2011-08-16 Quotient Package: make quotient_type work with separate set type
2011-05-15 wenzelm 2011-05-15 simplified/unified method_setup/attribute_setup;
2011-04-14 blanchet 2011-04-14 use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer
2011-03-13 wenzelm 2011-03-13 tuned headers;
2011-01-07 wenzelm 2011-01-07 more standard package setup;
2010-11-29 haftmann 2010-11-29 reorienting iff in Quotient_rel prevents simplifier looping; lemma QuotientI; tuned theory text
2010-11-29 haftmann 2010-11-29 moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; moved generic definitions about relations from Quotient.thy to Predicate; consistent use of R rather than E for relations; more natural deduction rules
2010-11-19 haftmann 2010-11-19 generalized type
2010-11-18 haftmann 2010-11-18 map_fun combinator in theory Fun
2010-11-09 haftmann 2010-11-09 type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
2010-10-19 Cezary Kaliszyk 2010-10-19 Quotient package: partial equivalence introduction
2010-10-05 blanchet 2010-10-05 remove needless Metis facts
2010-10-04 blanchet 2010-10-04 move Metis into Plain
2010-09-24 Cezary Kaliszyk 2010-09-24 quotient package: respectfulness and preservation of identity.
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-30 Cezary Kaliszyk 2010-08-30 Quotient Package: added respectfulness and preservation lemmas for mem.
2010-08-28 Christian Urban 2010-08-28 quotient package: lemmas to be lifted and descended can be pre-simplified
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.