src/HOL/Hilbert_Choice.thy
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