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