src/HOL/Hilbert_Choice.thy
5 weeks ago wenzelm 2019-03-14 more specific keyword kinds;
6 weeks ago haftmann 2019-03-05 avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
2 months ago haftmann 2019-01-31 proper congruence rule for image operator
3 months ago wenzelm 2019-01-06 isabelle update -u path_cartouches;
3 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
4 months ago haftmann 2018-12-19 tuned proof text
4 months ago haftmann 2018-12-19 tuned proof
5 months ago haftmann 2018-11-10 clarified status of legacy input abbreviations
7 months ago paulson 2018-09-11 A few new results, elimination of duplicates and more use of "pairwise"
7 months ago haftmann 2018-08-24 some modernization of notation
9 months ago nipkow 2018-07-11 moved lemmas
12 months ago Manuel Eberl 2018-03-26 Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
13 months ago Manuel Eberl 2018-03-12 Changes to complete distributive lattices due to Viorel Preoteasa
14 months ago paulson 2018-02-19 lots of new material, ultimately related to measure theory
14 months ago wenzelm 2018-02-15 more symbols;
23 months ago nipkow 2017-05-28 removed GreatestM
23 months ago nipkow 2017-05-28 introduced arg_max
23 months ago nipkow 2017-05-28 removed LeastM; is now arg_min
23 months ago nipkow 2017-05-14 added lemma
2016-12-17 haftmann 2016-12-17 restructured matter on polynomials and normalized fractions
2016-10-01 wenzelm 2016-10-01 tuned proofs;
2016-10-01 wenzelm 2016-10-01 Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
2016-09-05 wenzelm 2016-09-05 clarified obscure facts;
2016-08-08 wenzelm 2016-08-08 tuned proof;
2016-08-08 wenzelm 2016-08-08 tuned;
2016-08-05 wenzelm 2016-08-05 misc tuning and modernization;
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-04 haftmann 2016-07-04 dedicated locale for total bijections
2016-07-02 haftmann 2016-07-02 more theorems
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-21 wenzelm 2016-03-21 clarified rule structure;
2016-03-05 wenzelm 2016-03-05 old HOL syntax is for input only;
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-19 blanchet 2015-12-19 removed subsumed dependency
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-08-19 paulson 2015-08-19 New material and fixes related to the forthcoming Stone-Weierstrass development
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-26 wenzelm 2015-06-26 tuned whitespace;
2014-12-04 haftmann 2014-12-04 cleaned up mess
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-29 blanchet 2014-09-29 made 'moura' tactic more powerful
2014-08-28 blanchet 2014-08-28 renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
2014-08-28 blanchet 2014-08-28 moved skolem method
2014-06-30 hoelzl 2014-06-30 more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-04-26 haftmann 2014-04-26 tuned
2014-04-16 haftmann 2014-04-16 more simp rules for Fun.swap
2014-03-24 wenzelm 2014-03-24 removed unused 'ax_specification', to give 'specification' a chance to become localized; tuned whitespace;
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-01-20 blanchet 2014-01-20 moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
2014-01-16 blanchet 2014-01-16 dissolved 'Fun_More_FP' (a BNF dependency)
2013-12-15 haftmann 2013-12-15 more algebraic terminology for theories about big operators
2013-11-25 traytel 2013-11-25 eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
2013-11-10 haftmann 2013-11-10 qualifed popular user space names
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;