Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Relation.ML
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
Thu, 15 Oct 1998 11:38:39 +0200 paulson Uses overload_1st_set to specify overloading file | diff | annotate
Fri, 02 Oct 1998 14:28:39 +0200 nipkow id <-> Id file | diff | annotate
Wed, 19 Aug 1998 10:27:00 +0200 paulson Overloading decl should assist Blast_tac file | diff | annotate
Thu, 13 Aug 1998 18:14:26 +0200 paulson even more tidying of Goal commands file | diff | annotate
Fri, 31 Jul 1998 18:46:28 +0200 paulson new theorems for partial funcs file | diff | annotate
Wed, 15 Jul 1998 14:19:02 +0200 paulson More tidying and removal of "\!\!... from Goal commands file | diff | annotate
Wed, 15 Jul 1998 10:15:13 +0200 paulson Removal of leading "\!\!..." from most Goal commands file | diff | annotate
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal; file | diff | annotate
Mon, 27 Apr 1998 16:45:11 +0200 nipkow Added a few lemmas. file | diff | annotate
Mon, 30 Mar 1998 21:05:25 +0200 oheimb added introduction and elimination rules for Univalent file | diff | annotate
Mon, 16 Mar 1998 16:50:50 +0100 paulson inverse -> converse file | diff | annotate
Wed, 11 Mar 1998 11:05:14 +0100 paulson New theorem Image_eq_UN; deleted the silly vimage_inverse_Image file | diff | annotate
Tue, 03 Mar 1998 15:12:25 +0100 paulson New theorems; tidied file | diff | annotate
Wed, 25 Feb 1998 15:48:04 +0100 oheimb added split_all_tac to claset() file | diff | annotate
Mon, 23 Feb 1998 11:15:40 +0100 paulson New laws for id file | diff | annotate
Thu, 05 Feb 1998 10:48:43 +0100 paulson New theorem Image_id file | diff | annotate
Mon, 02 Feb 1998 12:55:39 +0100 paulson Three new facts about Image file | diff | annotate
Tue, 16 Dec 1997 17:58:03 +0100 wenzelm expandshort; file | diff | annotate
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp; file | diff | annotate
Fri, 26 Sep 1997 10:21:14 +0200 paulson Minor tidying to use Clarify_tac, etc. file | diff | annotate
Tue, 17 Jun 1997 09:01:56 +0200 nipkow converse -> ^-1 file | diff | annotate
Thu, 05 Jun 1997 14:39:22 +0200 nipkow Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. file | diff | annotate
Fri, 04 Apr 1997 11:18:52 +0200 paulson Calls Blast_tac file | diff | annotate
Sat, 15 Feb 1997 17:52:31 +0100 oheimb reflecting my recent changes of the simplifier and classical reasoner file | diff | annotate
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort file | diff | annotate
Thu, 12 Sep 1996 10:40:05 +0200 paulson Tidied many proofs, using AddIffs to let equivalences take file | diff | annotate
Fri, 28 Jun 1996 15:29:05 +0200 paulson Removed the unused rel_eq_cs file | diff | annotate
Mon, 03 Jun 1996 17:10:56 +0200 berghofe best_tac, deepen_tac and safe_tac now also use default claset. file | diff | annotate
Thu, 23 May 1996 15:15:20 +0200 berghofe Removed equalityI from some proofs (because it is now included file | diff | annotate
Tue, 21 May 1996 13:39:31 +0200 berghofe Replaced fast_tac by Fast_tac (which uses default claset) file | diff | annotate
Sat, 27 Apr 1996 12:07:31 +0200 nipkow Added R_O_id and id_O_R file | diff | annotate
Thu, 04 Apr 1996 11:45:01 +0200 paulson Using new "Times" infix file | diff | annotate
Mon, 25 Mar 1996 11:13:59 +0100 nipkow added converse_converse file | diff | annotate
Wed, 06 Mar 1996 12:52:11 +0100 paulson Ran expandshort file | diff | annotate
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs file | diff | annotate
Fri, 26 Jan 1996 20:25:39 +0100 nipkow Streamlined defs in Relation and added new intro/elim rules to do with file | diff | annotate
Wed, 04 Oct 1995 13:10:03 +0100 clasohm added local simpsets; removed IOA from 'make test' file | diff | annotate
Fri, 26 May 1995 18:11:47 +0200 nipkow Trancl is now based on Relation which used to be in Integ. file | diff | annotate
less more (0) tip
isabelle