src/HOL/Library/Quotient.thy
2004-05-06 wenzelm 2004-05-06 tuned document;
2001-12-05 wenzelm 2001-12-05 tuned;
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-02-12 wenzelm 2001-02-12 \<subseteq>;
2000-12-15 wenzelm 2000-12-15 GPLed;
2000-11-30 wenzelm 2000-11-30 renamed "equivalence_class" to "class";
2000-11-21 wenzelm 2000-11-21 unsymbolize;
2000-11-21 bauerg 2000-11-21 alternative function definition;
2000-11-18 wenzelm 2000-11-18 quot_cond_function: simplified, support conditional definition;
2000-11-17 wenzelm 2000-11-17 removed quot_cond_function1, quot_function1; removed overloaded standard operations;
2000-11-16 wenzelm 2000-11-16 added not_equiv_sym, not_equiv_trans1/2; tuned;
2000-11-15 wenzelm 2000-11-15 separate rules for function/operation definitions;
2000-11-12 wenzelm 2000-11-12 quot_cond_definition;
2000-11-10 wenzelm 2000-11-10 improved cong_definition theorems; overloaded standard operations;
2000-11-04 wenzelm 2000-11-04 tuned;
2000-11-03 wenzelm 2000-11-03 tuned;
2000-10-25 wenzelm 2000-10-25 tuned names;
2000-10-23 wenzelm 2000-10-23 tuned;
2000-10-22 wenzelm 2000-10-22 tuned;
2000-10-22 wenzelm 2000-10-22 simplified quotients (only plain total equivs);
2000-10-19 wenzelm 2000-10-19 improved typedef; tuned proofs;
2000-10-18 wenzelm 2000-10-18 Quotient types;