src/HOL/Hilbert_Choice.thy
Thu, 05 Aug 2021 07:12:49 +0000 haftmann clarified abstract and concrete boolean algebras
Wed, 05 May 2021 16:09:02 +0000 haftmann tuned theory structure
Sun, 11 Apr 2021 07:35:24 +0000 haftmann collected combinatorial material
Thu, 11 Mar 2021 07:05:38 +0000 haftmann avoid name clash
Sun, 28 Feb 2021 20:13:07 +0000 haftmann lemma diffusion
Mon, 11 May 2020 11:15:41 +0100 paulson the Uniq quantifier
Sun, 05 Apr 2020 17:12:26 +0100 paulson Tidied up more ancient, horrible proofs. Liberalised frac_le
Sat, 14 Mar 2020 15:58:51 +0000 paulson tidied up a few little proofs
Wed, 17 Apr 2019 21:53:45 +0100 paulson moved subset_image_inj into Hilbert_Choice
Wed, 10 Apr 2019 13:34:55 +0100 paulson The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
Thu, 14 Mar 2019 16:55:06 +0100 wenzelm more specific keyword kinds;
Tue, 05 Mar 2019 07:00:21 +0000 haftmann avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
Thu, 31 Jan 2019 13:08:59 +0000 haftmann proper congruence rule for image operator
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 19 Dec 2018 08:16:42 +0000 haftmann tuned proof text
Wed, 19 Dec 2018 08:16:41 +0000 haftmann tuned proof
Sat, 10 Nov 2018 07:57:19 +0000 haftmann clarified status of legacy input abbreviations
Tue, 11 Sep 2018 16:21:54 +0100 paulson A few new results, elimination of duplicates and more use of "pairwise"
Fri, 24 Aug 2018 20:22:14 +0000 haftmann some modernization of notation
Wed, 11 Jul 2018 01:04:23 +0200 nipkow moved lemmas
Mon, 26 Mar 2018 16:14:16 +0200 Manuel Eberl Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Mon, 12 Mar 2018 20:52:53 +0100 Manuel Eberl Changes to complete distributive lattices due to Viorel Preoteasa
Mon, 19 Feb 2018 16:44:45 +0000 paulson lots of new material, ultimately related to measure theory
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Sun, 28 May 2017 15:46:26 +0200 nipkow removed GreatestM
Sun, 28 May 2017 13:57:43 +0200 nipkow introduced arg_max
Sun, 28 May 2017 08:07:40 +0200 nipkow removed LeastM; is now arg_min
Sun, 14 May 2017 12:46:32 +0200 nipkow added lemma
Sat, 17 Dec 2016 15:22:13 +0100 haftmann restructured matter on polynomials and normalized fractions
Sat, 01 Oct 2016 19:29:48 +0200 wenzelm tuned proofs;
Sat, 01 Oct 2016 17:38:14 +0200 wenzelm Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
Mon, 05 Sep 2016 23:39:15 +0200 wenzelm clarified obscure facts;
Mon, 08 Aug 2016 19:34:00 +0200 wenzelm tuned proof;
Mon, 08 Aug 2016 18:55:12 +0200 wenzelm tuned;
Fri, 05 Aug 2016 18:14:28 +0200 wenzelm misc tuning and modernization;
Fri, 22 Jul 2016 11:00:43 +0200 wenzelm tuned proofs -- avoid unstructured calculation;
Mon, 04 Jul 2016 19:46:19 +0200 haftmann dedicated locale for total bijections
Sat, 02 Jul 2016 08:41:05 +0200 haftmann more theorems
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Mon, 21 Mar 2016 21:18:08 +0100 wenzelm clarified rule structure;
Sat, 05 Mar 2016 19:58:56 +0100 wenzelm old HOL syntax is for input only;
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Sat, 19 Dec 2015 20:02:51 +0100 blanchet removed subsumed dependency
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Thu, 27 Aug 2015 21:19:48 +0200 haftmann standardized some occurences of ancient "split" alias
Wed, 19 Aug 2015 19:18:19 +0100 paulson New material and fixes related to the forthcoming Stone-Weierstrass development
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Fri, 26 Jun 2015 10:20:33 +0200 wenzelm tuned whitespace;
Thu, 04 Dec 2014 16:51:54 +0100 haftmann cleaned up mess
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Mon, 29 Sep 2014 14:32:30 +0200 blanchet made 'moura' tactic more powerful
Thu, 28 Aug 2014 23:57:26 +0200 blanchet renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
Thu, 28 Aug 2014 16:58:27 +0200 blanchet moved skolem method
Mon, 30 Jun 2014 15:45:25 +0200 hoelzl more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
Wed, 18 Jun 2014 07:31:12 +0200 hoelzl moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
Sat, 26 Apr 2014 13:25:45 +0200 haftmann tuned
less more (0) -100 -60 tip