src/HOL/Hilbert_Choice.thy
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
Wed, 16 Apr 2014 21:51:41 +0200 haftmann more simp rules for Fun.swap
Mon, 24 Mar 2014 19:06:20 +0100 wenzelm removed unused 'ax_specification', to give 'specification' a chance to become localized;
Fri, 28 Feb 2014 17:54:52 +0100 traytel load Metis a little later
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Mon, 20 Jan 2014 23:07:23 +0100 blanchet moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
Thu, 16 Jan 2014 18:26:41 +0100 blanchet dissolved 'Fun_More_FP' (a BNF dependency)
Sun, 15 Dec 2013 15:10:14 +0100 haftmann more algebraic terminology for theories about big operators
Mon, 25 Nov 2013 10:14:29 +0100 traytel eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
Sun, 10 Nov 2013 15:05:06 +0100 haftmann qualifed popular user space names
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Fri, 16 Nov 2012 19:14:23 +0100 hoelzl moved (b)choice_iff(') to Hilbert_Choice
Sat, 20 Oct 2012 09:12:16 +0200 haftmann moved quite generic material from theory Enum to more appropriate places
Mon, 08 Oct 2012 12:03:49 +0200 haftmann consolidated names of theorems on composition;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 24 May 2012 17:25:53 +0200 wenzelm tuned proofs;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Sun, 20 Nov 2011 21:07:10 +0100 wenzelm eliminated obsolete "standard";
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Tue, 23 Nov 2010 14:14:17 +0100 hoelzl Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
Mon, 22 Nov 2010 10:34:33 +0100 hoelzl Replace surj by abbreviation; remove surj_on.
Tue, 05 Oct 2010 10:59:12 +0200 blanchet got rid of overkill "meson_choice" attribute;
Mon, 04 Oct 2010 21:55:54 +0200 blanchet remove Meson from Hilbert_Choice
Fri, 01 Oct 2010 14:01:29 +0200 blanchet added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Thu, 02 Sep 2010 11:29:02 +0200 blanchet use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Thu, 22 Oct 2009 09:27:48 +0200 nipkow inv_onto -> inv_into
less more (0) -60 tip