src/HOL/Relation.thy
Sat, 06 Sep 2014 20:12:32 +0200 haftmann added various facts
Thu, 29 May 2014 11:11:22 +0200 nipkow typo
Tue, 29 Apr 2014 16:02:02 +0200 wenzelm prefer plain ASCII / latex over not-so-universal Unicode;
Sat, 26 Apr 2014 14:53:22 +0200 haftmann more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
Sat, 12 Apr 2014 11:27:36 +0200 haftmann more operations and lemmas
Wed, 19 Mar 2014 18:47:22 +0100 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
Thu, 13 Mar 2014 13:18:13 +0100 blanchet killed a few 'metis' calls
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Tue, 21 Jan 2014 13:21:55 +0100 traytel removed theory dependency of BNF_LFP on Datatype
Mon, 20 Jan 2014 20:21:12 +0100 blanchet move BNF_LFP up the dependency chain
Fri, 29 Nov 2013 08:26:45 +0100 traytel set_comprehension_pointfree simproc causes to many surprises if enabled by default
Thu, 21 Nov 2013 21:33:34 +0100 blanchet rationalize imports
Tue, 12 Nov 2013 19:28:51 +0100 hoelzl countability of the image of a reflexive transitive closure
Fri, 18 Oct 2013 10:43:20 +0200 blanchet killed most "no_atp", to make Sledgehammer more complete
Tue, 17 Sep 2013 08:42:51 +0200 nipkow added lemmas and made concerse executable
Sun, 28 Jul 2013 12:59:59 +0200 traytel more converse(p) theorems; tuned proofs;
Thu, 25 Jul 2013 12:25:07 +0200 traytel two useful relation theorems
Wed, 19 Jun 2013 10:06:24 +0200 nipkow added lemma
Fri, 07 Dec 2012 15:53:28 +0100 nipkow corrected nonsensical associativity of `` and dvd
Tue, 31 Jul 2012 13:55:39 +0200 kuncar more relation operations expressed by Finite_Set.fold
Thu, 12 Jul 2012 16:22:33 +0200 bulwahn a first guess to avoid the Codegenerator_Test to loop infinitely
Wed, 16 May 2012 19:17:20 +0200 kuncar generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
Thu, 12 Apr 2012 11:01:15 +0200 bulwahn merged
Tue, 03 Apr 2012 17:45:06 +0900 griff dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
Tue, 03 Apr 2012 17:26:30 +0900 griff renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
Thu, 05 Apr 2012 15:23:26 +0200 huffman define reflp directly, in the manner of symp and transp
Thu, 22 Mar 2012 18:54:39 +0100 haftmann fixed typo
Sat, 17 Mar 2012 11:35:18 +0100 haftmann spelt out missing colemmas
Sat, 17 Mar 2012 08:00:18 +0100 haftmann generalized INF_INT_eq, SUP_UN_eq
Mon, 12 Mar 2012 21:41:11 +0100 noschinl tuned proofs
Mon, 12 Mar 2012 15:12:22 +0100 noschinl tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
Mon, 12 Mar 2012 15:11:24 +0100 noschinl tuned simpset
Wed, 07 Mar 2012 21:34:36 +0100 haftmann tuned syntax; more candidates
Fri, 02 Mar 2012 21:45:45 +0100 haftmann more fundamental pred-to-set conversions for range and domain by means of inductive_set
Thu, 01 Mar 2012 19:34:52 +0100 haftmann more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
Sun, 26 Feb 2012 21:44:12 +0100 haftmann restored accidental omission
Sun, 26 Feb 2012 21:26:28 +0100 haftmann tuned structure
Sun, 26 Feb 2012 20:43:33 +0100 haftmann tuned structure; dropped already existing syntax declarations
Sun, 26 Feb 2012 20:10:14 +0100 haftmann tuned syntax declarations; tuned structure
Sun, 26 Feb 2012 15:28:48 +0100 haftmann marked candidates for rule declarations
Fri, 24 Feb 2012 22:46:44 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Fri, 24 Feb 2012 09:40:02 +0100 haftmann given up disfruitful branch
Fri, 24 Feb 2012 08:49:36 +0100 haftmann explicit remove of lattice notation
Thu, 23 Feb 2012 21:25:59 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Mon, 30 Jan 2012 21:49:41 +0100 nipkow added "'a rel"
Sun, 01 Jan 2012 11:28:45 +0100 haftmann cleanup of code declarations
Sat, 24 Dec 2011 15:53:09 +0100 haftmann dropped obsolete code equation for Id
Thu, 13 Oct 2011 23:02:59 +0200 haftmann moved acyclic predicate up in hierarchy
Thu, 13 Oct 2011 22:56:19 +0200 haftmann modernized definitions
Tue, 20 Sep 2011 21:47:52 +0200 haftmann tuned specification and lemma distribution among theories; tuned proofs
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Thu, 18 Aug 2011 13:55:26 +0200 haftmann observe distinction between sets and predicates more properly
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Tue, 07 Dec 2010 13:33:28 +0100 bulwahn adding a definition for refl_on which is friendly for quickcheck and nitpick
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adding a nice definition of Id_on for quickcheck and nitpick
Sun, 09 May 2010 12:00:43 +0200 krauss added lemmas rel_comp_UNION_distrib(2)
Fri, 07 May 2010 15:03:57 +0200 krauss removed semicolons
Fri, 07 May 2010 15:03:53 +0200 krauss rule subrelI (for nice Isar proofs of relation inequalities)
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Mon, 26 Oct 2009 23:27:24 +0100 krauss lemma converse_inv_image
less more (0) -100 -60 tip