src/HOL/Hilbert_Choice.thy
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
2006-11-08 wenzelm 2006-11-08 removed theory NatArith (now part of Nat);
2006-10-13 berghofe 2006-10-13 Adapted to changes in FixedPoint theory.
2005-12-13 paulson 2005-12-13 removal of functional reflexivity axioms
2005-10-18 wenzelm 2005-10-18 added lemma exE_some (from specification_package.ML);
2005-09-29 wenzelm 2005-09-29 more finalconsts;
2005-09-15 paulson 2005-09-15 comment
2005-07-13 paulson 2005-07-13 generlization of some "nat" theorems
2005-06-24 paulson 2005-06-24 meson method taking an argument list
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-06-05 wenzelm 2004-06-05 improved symbolic syntax of Eps: \<some> for mode "epsilon";
2004-05-19 paulson 2004-05-19 conversion of Hilbert_Choice to Isar script
2004-02-19 ballarin 2004-02-19 New lemmas about inversion of restricted functions. HOL-Algebra: new locale "ring" for non-commutative rings.
2003-09-26 paulson 2003-09-26 misc tidying
2003-07-17 skalberg 2003-07-17 Added package for definition by specification.
2002-12-22 nipkow 2002-12-22 removed some problems with print translations
2002-12-22 nipkow 2002-12-22 added print translations tha avoid eta contraction for important binders.
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2001-12-05 wenzelm 2001-12-05 tuned declarations;
2001-11-26 wenzelm 2001-11-26 tuned; meson lemmas from Tools/meson.ML;
2001-11-03 wenzelm 2001-11-03 tuned;
2001-08-29 wenzelm 2001-08-29 avoid ML bindings;
2001-07-25 paulson 2001-07-25 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice