src/HOL/Hilbert_Choice.thy
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;
2012-11-16 hoelzl 2012-11-16 moved (b)choice_iff(') to Hilbert_Choice
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-10-08 haftmann 2012-10-08 consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-05-24 wenzelm 2012-05-24 tuned proofs;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-09-13 huffman 2011-09-13 tuned proofs
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2010-11-23 hoelzl 2010-11-23 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
2010-11-22 hoelzl 2010-11-22 Replace surj by abbreviation; remove surj_on.
2010-10-05 blanchet 2010-10-05 got rid of overkill "meson_choice" attribute; tuning
2010-10-04 blanchet 2010-10-04 remove Meson from Hilbert_Choice
2010-10-01 blanchet 2010-10-01 added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-09-02 blanchet 2010-09-02 use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2009-10-22 nipkow 2009-10-22 inv_onto -> inv_into
2009-10-20 nipkow 2009-10-20 added inv_def for compatibility as a lemma
2009-10-18 nipkow 2009-10-18 Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-04 haftmann 2009-06-04 dropped legacy ML bindings; tuned
2009-06-02 haftmann 2009-06-02 added/moved lemmas by Andreas Lochbihler
2009-01-28 haftmann 2009-01-28 Plain, Main form meeting points in import hierarchy
2008-08-06 nipkow 2008-08-06 added lemma
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2008-04-07 paulson 2008-04-07 * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
2008-03-20 haftmann 2008-03-20 tuned proofs
2008-02-21 nipkow 2008-02-21 moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and added some
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2007-06-20 nipkow 2007-06-20 added lemmas
2007-04-15 wenzelm 2007-04-15 replaced axioms/finalconsts by proper axiomatization;
2007-01-04 paulson 2007-01-04 improvements to proof reconstruction. Some files loaded in a different order