| Thu, 10 Oct 2002 14:23:19 +0200 | berghofe | Removed obsolete function "fun_rel_comp". | file | diff | annotate |
| Wed, 20 Feb 2002 15:47:42 +0100 | berghofe | Converted to new theory format. | file | diff | annotate |
| Thu, 13 Dec 2001 16:47:35 +0100 | nipkow | comp -> rel_comp | file | diff | annotate |
| Wed, 03 Oct 2001 20:54:16 +0200 | wenzelm | tuned parentheses in relational expressions; | file | diff | annotate |
| Wed, 25 Jul 2001 13:13:01 +0200 | paulson | partial restructuring to reduce dependence on Axiom of Choice | file | diff | annotate |
| Thu, 15 Feb 2001 16:00:40 +0100 | oheimb | moved inv_image to Relation | file | diff | annotate |
| Tue, 09 Jan 2001 15:22:13 +0100 | nipkow | `` -> and ``` -> `` | file | diff | annotate |
| Fri, 05 Jan 2001 18:48:18 +0100 | nipkow | ^^ -> ``` | file | diff | annotate |
| Fri, 05 Jan 2001 10:19:14 +0100 | paulson | Field of a relation, and some Domain/Range rules | file | diff | annotate |
| Fri, 15 Sep 2000 12:39:57 +0200 | paulson | renamed (most of...) the select rules | file | diff | annotate |
| Fri, 23 Jun 2000 10:43:43 +0200 | paulson | new theorem trans_O_subset | file | diff | annotate |
| Thu, 22 Jun 2000 23:04:34 +0200 | wenzelm | bind_thm(s); | file | diff | annotate |
| Wed, 21 Jun 2000 10:31:34 +0200 | paulson | generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split | file | diff | annotate |
| Thu, 13 Apr 2000 15:01:50 +0200 | nipkow | Times -> <*> | file | diff | annotate |
| Mon, 21 Feb 2000 13:57:07 +0100 | oheimb | renamed Univalent to univalent | file | diff | annotate |
| Mon, 21 Feb 2000 10:20:38 +0100 | nipkow | A few lemmas and some Adds. | file | diff | annotate |
| Mon, 31 Jan 2000 16:18:42 +0100 | paulson | new theorem rev_ImageI | file | diff | annotate |
| Thu, 11 Nov 1999 10:24:14 +0100 | paulson | Fixed obsolete use of "op ^^"; new lemma | file | diff | annotate |
| Fri, 22 Oct 1999 18:26:46 +0200 | paulson | new theorems on Image | file | diff | annotate |
| Mon, 11 Oct 1999 10:49:18 +0200 | paulson | new thm Domain_mono | file | diff | annotate |
| Mon, 26 Jul 1999 16:29:38 +0200 | paulson | three new theorems | file | diff | annotate |
| Mon, 19 Jul 1999 15:24:35 +0200 | paulson | getting rid of qed_goal | file | diff | annotate |
| Fri, 16 Jul 1999 12:09:48 +0200 | berghofe | Added some definitions and theorems needed for the | file | diff | annotate |
| Thu, 15 Jul 1999 10:27:54 +0200 | paulson | qed_goal -> Goal | file | diff | annotate |
| Thu, 10 Jun 1999 10:35:58 +0200 | paulson | new preficates refl, sym [from Integ/Equiv], antisym | file | diff | annotate |
| Wed, 02 Dec 1998 15:52:39 +0100 | paulson | new theorems Domain_Union, Range_Union | file | diff | annotate |
| Tue, 01 Dec 1998 10:39:02 +0100 | paulson | better version of Image_diag | file | diff | annotate |
| Mon, 30 Nov 1998 10:43:35 +0100 | paulson | new theorems about diag | file | diff | annotate |
| Fri, 27 Nov 1998 10:40:29 +0100 | paulson | moved diag (diagonal relation) from Univ to Relation | file | diff | annotate |
| Mon, 09 Nov 1998 11:00:44 +0100 | paulson | new Domain/Range rules | file | diff | annotate |