src/HOL/Hilbert_Choice.thy
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
Tue, 20 Oct 2009 13:20:42 +0200 nipkow added inv_def for compatibility as a lemma
Sun, 18 Oct 2009 12:07:25 +0200 nipkow Inv -> inv_onto, inv abbr. inv_onto UNIV.
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Thu, 04 Jun 2009 15:28:58 +0200 haftmann dropped legacy ML bindings; tuned
Tue, 02 Jun 2009 16:23:43 +0200 haftmann added/moved lemmas by Andreas Lochbihler
Wed, 28 Jan 2009 11:03:42 +0100 haftmann Plain, Main form meeting points in import hierarchy
Wed, 06 Aug 2008 13:57:25 +0200 nipkow added lemma
Fri, 25 Apr 2008 15:30:33 +0200 krauss Merged theories about wellfoundedness into one: Wellfounded.thy
Mon, 07 Apr 2008 15:37:27 +0200 paulson * 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.
Thu, 20 Mar 2008 12:01:09 +0100 haftmann tuned proofs
Thu, 21 Feb 2008 17:33:58 +0100 nipkow moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
Fri, 15 Feb 2008 16:09:12 +0100 haftmann <= and < on nat no longer depend on wellfounded relations
Wed, 20 Jun 2007 14:38:24 +0200 nipkow added lemmas
Sun, 15 Apr 2007 14:31:44 +0200 wenzelm replaced axioms/finalconsts by proper axiomatization;
Thu, 04 Jan 2007 17:55:12 +0100 paulson improvements to proof reconstruction. Some files loaded in a different order
Wed, 08 Nov 2006 13:48:29 +0100 wenzelm removed theory NatArith (now part of Nat);
Fri, 13 Oct 2006 18:15:18 +0200 berghofe Adapted to changes in FixedPoint theory.
Tue, 13 Dec 2005 15:27:43 +0100 paulson removal of functional reflexivity axioms
Tue, 18 Oct 2005 17:59:26 +0200 wenzelm added lemma exE_some (from specification_package.ML);
Thu, 29 Sep 2005 00:58:55 +0200 wenzelm more finalconsts;
Thu, 15 Sep 2005 17:44:53 +0200 paulson comment
Wed, 13 Jul 2005 15:06:20 +0200 paulson generlization of some "nat" theorems
Fri, 24 Jun 2005 17:25:10 +0200 paulson meson method taking an argument list
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 19 Oct 2004 18:18:45 +0200 paulson converted some induct_tac to induct
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Sat, 05 Jun 2004 13:07:04 +0200 wenzelm improved symbolic syntax of Eps: \<some> for mode "epsilon";
Wed, 19 May 2004 11:29:47 +0200 paulson conversion of Hilbert_Choice to Isar script
Thu, 19 Feb 2004 16:44:21 +0100 ballarin New lemmas about inversion of restricted functions.
less more (0) -60 tip