src/HOL/Relation.thy
Thu, 11 Jun 2020 16:13:53 +0100 paulson fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
Mon, 11 May 2020 11:15:41 +0100 paulson the Uniq quantifier
Mon, 27 Jan 2020 14:32:43 +0000 paulson A few lemmas connected with orderings
Sun, 10 Mar 2019 15:16:45 +0000 haftmann dropped superfluous declaration attribute
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sat, 10 Nov 2018 07:57:19 +0000 haftmann clarified status of legacy input abbreviations
Sat, 16 Jun 2018 20:32:00 +0200 nipkow moved lemmas from AFP
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Wed, 16 Aug 2017 21:14:11 +0200 nipkow more reorganization around sorted_wrt
Tue, 15 Aug 2017 19:47:08 +0200 nipkow added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
Thu, 22 Dec 2016 08:43:30 +0100 haftmann proper logical constants
Wed, 21 Dec 2016 21:26:26 +0100 haftmann prefer existing logical constant over abbreviation
Wed, 21 Dec 2016 21:26:26 +0100 haftmann dropped aliasses
Sat, 17 Dec 2016 15:22:00 +0100 haftmann added lemmas demanded by FIXMEs
Fri, 05 Aug 2016 18:14:28 +0200 wenzelm misc tuning and modernization;
Fri, 29 Jul 2016 12:44:22 +0200 Andreas Lochbihler prefer [simp] over [iff] as [iff] break HOL-UNITY
Fri, 29 Jul 2016 09:49:23 +0200 Andreas Lochbihler add lemmas contributed by Peter Gammie
Wed, 06 Jul 2016 20:19:51 +0200 wenzelm misc tuning and modernization;
Mon, 04 Jul 2016 19:46:20 +0200 haftmann default one-step rules for predicates on relations;
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Thu, 07 Jan 2016 17:40:55 +0000 paulson revisions to limits and derivatives, plus new lemmas
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 11 Nov 2015 09:48:24 +0100 Andreas Lochbihler add various lemmas
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 14 Apr 2015 11:32:01 +0200 Andreas Lochbihler add lemmas
Wed, 11 Feb 2015 14:07:28 +0100 Andreas Lochbihler add lemma
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
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
less more (0) -100 -60 tip