src/HOL/Hilbert_Choice_lemmas.ML
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-10 wenzelm 2001-12-10 bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
2001-12-05 wenzelm 2001-12-05 tuned declarations;
2001-08-06 paulson 2001-08-06 tidying and moving the theorem "choice"
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