src/HOL/Library/Quotient.thy
Fri, 15 Dec 2000 17:59:45 +0100 wenzelm GPLed;
Thu, 30 Nov 2000 20:05:34 +0100 wenzelm renamed "equivalence_class" to "class";
Tue, 21 Nov 2000 19:03:06 +0100 wenzelm unsymbolize;
Tue, 21 Nov 2000 11:31:45 +0100 bauerg alternative function definition;
Sat, 18 Nov 2000 19:46:48 +0100 wenzelm quot_cond_function: simplified, support conditional definition;
Fri, 17 Nov 2000 18:48:50 +0100 wenzelm removed quot_cond_function1, quot_function1;
Thu, 16 Nov 2000 19:03:26 +0100 wenzelm added not_equiv_sym, not_equiv_trans1/2;
Wed, 15 Nov 2000 19:43:42 +0100 wenzelm separate rules for function/operation definitions;
Sun, 12 Nov 2000 14:50:26 +0100 wenzelm quot_cond_definition;
Fri, 10 Nov 2000 19:06:30 +0100 wenzelm improved cong_definition theorems;
Sat, 04 Nov 2000 18:41:37 +0100 wenzelm tuned;
Fri, 03 Nov 2000 21:35:59 +0100 wenzelm tuned;
Wed, 25 Oct 2000 18:33:01 +0200 wenzelm tuned names;
Mon, 23 Oct 2000 22:11:43 +0200 wenzelm tuned;
Sun, 22 Oct 2000 22:23:16 +0200 wenzelm tuned;
Sun, 22 Oct 2000 22:18:40 +0200 wenzelm simplified quotients (only plain total equivs);
Thu, 19 Oct 2000 21:23:15 +0200 wenzelm improved typedef;
Wed, 18 Oct 2000 23:29:13 +0200 wenzelm Quotient types;
less more (0) tip